IEEE Spectrum: AI v matematike núti k veľkým otázkam

Čo sa stalo

IEEE Spectrum 27. júna publikoval analýzu, ako AI modely (najmä Gemini, GPT-5.x a Claude) dosahujú na výskumnú úroveň v matematike — riešia open problémy, generujú dokazovacie kandidáty a niektoré aj nezávisle objavujú lemy.

Kontext a dopad

Komunita matematiky musí zvážiť: čo znamená 'dokázať' výsledok, ak ho generuje LLM? Ako verifikovať? Bude AI nahrádzať mladých matematikov, alebo ich akcelerovať? Otvára aj otázku autorstva a peer-review konvencií.

Detaily

• Citované sú úspechy AlphaProof, Lean kopilotov a frontier LLMs
• Niektorí matematici hlásia, že LLM už generujú netriviálne lemy
• Diskusia o formalizácii (Lean, Coq) ako 'machine-verifiable' štandard
• Hrozba: hromady wrong 'proofs' zaplavia journals
• Šanca: kolaborácia ľudia + AI by mohla obísť celé generácie matematiky