Why hasn’t OpenAI figured out the abc conjecture yet? I remember a few years ago Mochizuki was fighting with Scholze-Stix about how they just didn’t understand him even though Scholze was a Fields medalist. Can’t ChatGPT frontier models just settle this? they already did a lot other presumably more difficult stuff than just to check one previously-claimed proof. right?
>>17082433Mochizuki is a great mathematician.I would be appalled if OpenAI violates his masterpiece by formally verifying it.
>>17082433too busy working on the bbc conjecture
>>17082433He's an exemplar of why AI proofs will always fail: if you translate something into a new language and prove something about it in translation, there's a very good chance you didn't prove the same thing in the original language.I also don't believe that Wiles' elliptically translated proof satisfies Fermat's conjecture, for the same reason. I suspect more and more people will find my disbelief more and more attractive as time goes on and lean diarrhea continues to pile up.
