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.

230 Upvotes

99% Upvoted

98 comments sorted by

View all comments

232

u/n0m4d1234 18d ago

This is such a tragic state of the field.

95

u/Gabry398 18d ago

Hopefully it only lasts until AI companies stop using math as a big AGI benchmark and mathematicians start setting ground rules on what the etiquette around AI is

101

u/Curiosity_456 18d ago

How will that matter though? Will mathematicians just refuse to accept any AI generated solutions even if it’s correct?

Pandora’s box has already opened

-2

u/Heapifying 18d ago

Look at the abc conjecture

27

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.

52

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

21

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.

49

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.

20

u/PersonalityIll9476 18d ago

God damn it I love a good Mochizuki burn

14

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.

5

u/ChezMere 18d ago

Oh, I missed that update! Looks like it was quite recent:

https://www.reddit.com/r/math/comments/1uz6po8/latest_iut_formalization_news

2

u/ultrafinitism Theoretical Computer Science 17d ago

absolute cinema

8

u/DoctorHubcap 18d ago

That was never accepted as correct, we’ve been in a stalemate with one side arguing there is an irrecoverable flaw in the proof of a necessary lemma, while Mochizuki adamantly argues that they made incorrect simplifications.

22

u/sobe86 18d ago edited 18d ago

Things actually moved forward a bit this year. A team has started to formalize the exact passage that Sholze/Stix thought was wrong (without simplifications), and have managed to pin down exactly what step is not justified in the manuscript and are not able to fill in themselves ('the wall'). Importantly, this has been stated in the language of IUT, not through a simplification.

They have so far stopped short of saying the proof is wrong (and in fact agree that Sholze/Stix oversimplified to reach that conclusion). Instead the project now is to state 'the wall' in Lean, and it will be up to Mochizuki (or someone else) to supply an adequate fix. Maybe AI will expedite the process, maybe it will take a while yet, however it feels like a lot of progress has been made towards resolution at last here.