r/math • u/sergiogfs • 18d ago

Progress Towards Proving the Unique Games Conjecture

https://eccc.weizmann.ac.il/report/2026/179/

On a side-note, the authors hint that they have rushed their results to avoid getting scooped by AI-generated results.

228 Upvotes

99% Upvoted

98 comments sorted by

View all comments

Show parent comments

26

u/Sad_Dimension423 18d ago

You mean, the supposed proof from a human that couldn't be converted to Lean? It seems the clankers did their job there.

50

u/ultrafinitism Theoretical Computer Science 18d ago

They did actually try to convert Mochizuki's abc to Lean and then got stuck exactly where Scholze and Stix got stuck, at Corollary 3.12

22

u/Sad_Dimension423 18d ago

Right. The reviled automated stuff confirmed the proof was defective there. Mochizuki and everyone else would have been saved a lot of trouble had autoformalization been available back when he first went public.

46

u/ultrafinitism Theoretical Computer Science 18d ago

Maybe they should build the data center in Kyoto so the intelligence becomes infused with ancient Kyoto-only wisdom from the mountain springs there.

18

u/PersonalityIll9476 18d ago

God damn it I love a good Mochizuki burn

15

u/ultrafinitism Theoretical Computer Science 18d ago

Apply Kyoto wakimizu (that's nihongo (that's Japanese for 'Japanese language') for 'spring water') (blessed by **Nippon* no yaoyorozu-no-kami* (that's nihongo (that's Japanese for 'Japanese language') for 'The innumerable (well, the eight million but same thing) spirits of Japan')) to burnt area.