Matematici nasadili AI na formalizáciu Fermátovej poslednej vety v Leane

Čo sa stalo

Matematici vrátane Kevina Buzzarda z Imperial College London spustili workshop na zabudovanie formálneho dôkazu Fermátovej poslednej vety do knižnice Mathlib pre proof assistant Lean — s výraznou pomocou AI nástrojov.

Kontext a dopad

Fermátovu poslednú vetu dokázal Andrew Wiles v roku 1993, no dôkaz nikdy nebol formálne strojovo verifikovaný. Projekt má symbolický aj praktický rozmer: AI sa stáva akcelerátorom formálnej matematiky. Otvára filozofickú otázku — ak stroj verifikuje dôkaz, ktorý ľudia v celom rozsahu nerozumejú, čo sme dosiahli?

Detaily

• Vedúci projektu: Kevin Buzzard, Imperial College London
• Cieľ: zabudovanie Fermátovej poslednej vety do Mathlib (Lean proof assistant)
• Výsledok prvého dňa: kódová základňa vzrástla z 20 000 na 40 000 riadkov
• AI úloha: asistencia pri písaní formálnych dôkazov a refaktoringu kódu
• Workshop: zjednotil matematikov, informatikov a AI špecialistov v Londýne