If I recall correctly there was a proposed proof to the abc conjecture by Mochizuki https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs which was rejected due to being rather inpenetrable to humans. Shouldn't this be an ideal target for LLMs?
There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect.
But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).
It was rejected for being wrong (or most charitably, incomplete).
Similarly, I'd love to see LLMs create a formal proof of the https://en.wikipedia.org/wiki/Classification_of_finite_simpl...
I’d like to see four color conjecture and an elementary proof of FLT.