AI poráža ľudských matematikov v objavovaní protikladov: desaťročia staré problémy vyriešené

Čo sa stalo

Frontier AI modely (Claude Fable, ChatGPT Sol) rýchlo vyriešili desaťročia staré otvorené matematické problémy generovaním formálnych protikladov — vrátane vyvrátenia Erdősovej Unit Distance conjecture a 60-ročnej Grothendieck otázky o group schemes. Všetky výsledky boli formálne overené v Lean.

Kontext a dopad

Kevin Buzzard (Imperial College, Xena Project) argumentuje, že 'veľké AI-generované matematické objavy sú nevyhnutné' a tempo formálne overených AI dôkazov rastie na tisíce riadkov týždenne. Toto vyvoláva fundamentálne prehodnocovanie toho, čo tvorí matematický objav a aká je budúcnosť ľudských matematikov — najmä v kontexte, keď USA škrtia financovanie matematického výskumu.

Detaily

• Vyvrátená Erdősova Unit Distance conjecture (stará desaťročia)
• Nájdené protiklady k 60-ročnej Grothendieck otázke o group schemes
• Všetky výsledky formálne verifikované v Lean theorem proveri
• Tempo: AI generuje tisíce riadkov formálnych dôkazov týždenne
• Autor Buzzard: 'veľké AI matematické objavy sú nevyhnutné'
• Implikácia: spochybňuje samotnú definíciu 'matematického objavu'