logoalt Hacker News

a_imhotoday at 2:18 PM2 repliesview on HN

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?


Replies

lg5689today at 6:48 PM

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

anorwelltoday at 3:12 PM

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