This kind of papers go way over my head, but recently I was surprised that ChatGTP (free) found the proof for an expression had a square value for some variables. It dug up a relationship from a paper from 2009 and correctly applied it to the case.

The chat: https://chatgpt.com/share/6a7f1b08-b9dc-83ea-b911-aaf8b65f1c...