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.
>>17082433Corollary 3.12. It's flawed. That retard won't provide additional reasoning to explain why it's true. You can't formalize with incomplete reasoning. If you can prove this one the rest of proof automatically follows.
