It was rejected for being wrong (or most charitably, incomplete).

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).

Similarly, I'd love to see LLMs create a formal proof of the https://en.wikipedia.org/wiki/Classification_of_finite_simpl...