Fermatova poslední věta zní jako věc z učebnice, která už má dávno odpracováno. Právě proto mě zaujala zpráva, že Claude měl během 11 dní vytvořit její kompletní počítačem ověřený důkaz. Nejde jen o matematickou kuriozitu: podobné postupy by jednou mohly ušetřit lidem dost úmorné práce s kontrolou důkazů.
Starý problém, jiný druh kontroly
Fermatova poslední věta tvrdí, velmi zjednodušeně, že pro celočíselné exponenty větší než dvě neexistují nenulová celá čísla, která by splnila rovnici xn + yn = zn. Andrew Wiles ji ručně dokázal v roce 1995. Jenže mezi lidsky čitelným matematickým důkazem a důkazem, který beze zbytku projde kontrolou počítače, vede dost dlouhá cesta.
TLDR píše, že Claude důkaz formalizoval v Lean. Lean je systém, v němž se matematika zapisuje tak přesně, aby jednotlivé kroky mohl ověřit počítač. Výsledný projekt měl mít 13 milionů řádků kódu a obsahovat důkazy 29 500 mezitvrzení. Ta čísla jsou tak velká, že jsem si nejdřív představila, jak se někdo pokusil otevřít soubor v běžném editoru a ventilátor notebooku okamžitě vyhlásil stávku.
Ověření mělo proběhnout přes Prove2Me a Lean. Z podkladu ale neplyne, kde je celý důkaz veřejně dostupný, kdo přesně kontrolu provedl ani zda jej nezávisle zopakoval další tým. To jsou pro mě dost podstatné detaily. U tak velkého tvrzení bych si ráda přečetla i původní technickou zprávu, ne jen stručné shrnutí v newsletteru.
Nejde o to, že AI „porazila“ Wilesa
Mně osobně přijde trochu zavádějící stavět vedle sebe Claude a Wilesa, jako by oba soutěžili ve stejné disciplíně. Wiles musel najít samotnou cestu k důkazu; Claude měl podle popisu automatizovat formalizaci už známého výsledku. I to je ale velká práce, protože formální ověřování vyžaduje rozebrat argument na množství drobných kroků, které systém přijme bez domýšlení.
Právě zde vidím nejzajímavější praktickou stránku. Matematici mohou mít správný nápad, ale převést jej do formálního systému je časově náročné. Model, který umí pomoci s tisíci mezikroky, by mohl fungovat spíš jako velmi rychlý a puntičkářský pomocník než jako osamělý génius s tabulí. Věta „to přece z předchozího kroku jasně plyne“ na něj nejspíš nezabere, což je v matematice vlastně jeho sympatická vlastnost.
Formální důkaz není automaticky porozumění
Počítačové ověření má obrovskou hodnotu: pokud jsou zápis a kontrolní jádro správně, systém ověří, že každý formální krok navazuje na předchozí. Neznamená to ovšem samo o sobě, že model rozuměl matematice stejným způsobem jako člověk nebo že by bez zadání dokázal přijít s novou hlubokou teorií.
Zpráva je pro mě zajímavá hlavně jako ukázka směru. AI se nemusí prosadit jen tam, kde napíše plynulý odstavec nebo obrázek. Může být užitečná i v prostředích, kde se každé tvrzení dá tvrdě zkontrolovat. A to je příjemná změna proti situacím, v nichž model sebevědomě vysvětlí něco, co si právě vymyslel.
Celý údajný důkaz bych zatím brala s opatrností, dokud neuvidím podrobnější primární podklady a nezávislé ověření. Samotná představa, že se formalizace složitých důkazů může z práce na celé roky zkrátit na dny, je ale dost lákavá na to, abych jí věnovala pozornost.
