Anthropic zveřejnil repozitář s formálním důkazem Velké Fermatovy věty. Několik desítek agentů Claude převedlo variantu klasického argumentu Wilese, Taylora a dalších do jazyka Lean, v němž počítač kontroluje každý logický krok. Projekt podle firmy trval jedenáct dní, vytvořil přibližně 13 milionů řádků a v konečné větvi použil asi 29 500 pomocných vět.

Důležité je nepřecenit význam slova „důkaz“. Claude neobjevil nové řešení problému, který byl vyřešen už v 90. letech. Novinkou je úplný strojově kontrolovatelný převod rozsáhlé moderní matematiky. Výsledek navazuje na léta práce komunity Lean, Mathlib a projektu vedeného Kevinem Buzzardem; jeho kladné odborné vyjádření je důležitá kontrola, ale širší nezávislé prověřování tak obrovského artefaktu teprve začne.

Agenti uspěli až s platformou Prove2Me, která rozdělila cíl do grafu menších vět, udržovala stav projektu a umožňovala hotové části znovu používat. Výsledek tak vypovídá nejen o modelu, ale i o kvalitě orchestrace, knihoven a lidsky připraveného matematického základu. Repozitář je veřejný pod licencí Apache 2.0, takže jej mohou další týmy kontrolovat a rozvíjet.

Pokud se metoda osvědčí i mimo tento ukázkový případ, mohla by pomáhat převádět odborné články do kontrolovatelné podoby, odhalovat skryté mezery a prověřovat rychle rostoucí množství matematiky vytvořené s AI. V delším výhledu by formální certifikáty mohly doprovázet výsledky používané v kryptografii, verifikaci čipů nebo bezpečnostně kritickém softwaru. Pořád však nenahradí srozumitelný výklad ani lidské posouzení, zda byly zvoleny správné předpoklady.

Pro praxi je nutné zmenšit extrémní objem kódu a spotřebu, reprodukovat kontrolu nezávislými nástroji a ukázat spolehlivost na nových důkazech bez tak bohaté existující infrastruktury. Optimisticky lze během 1–3 let čekat užitečné asistenty pro formalizační týmy a do 3–7 let formální přílohy u části matematických publikací. Rutinní automatická kontrola většiny nové matematiky je vzdálenější a její termín dnes nelze věrohodně určit.