Axiom afferma che agenti IA hanno formalizzato in Lean la classificazione dei gruppi semplici finiti

Axiom, azienda di matematica basata sull’IA, ha annunciato su X una formalizzazione automatica completa in Lean della classificazione dei gruppi semplici finiti, un risultato che definisce la «tavola periodica della simmetria». Descrive la dimostrazione originale come composta da circa 15.000 pagine, scritte da oltre 100 matematici nel corso di più generazioni, e la definisce la più grande dimostrazione matematica della storia verificata al computer.

Secondo il repository open source di Axiom, sciami di agenti IA hanno prodotto circa 43,1 milioni di righe di codice Lean in 24 giorni, coprendo 715 articoli e libri e segnalando 34 discrepanze rispetto alla documentazione pubblicata. Un post dell’account di notizie sull’IA TestingCatalog aggiunge che gli agenti hanno suddiviso il lavoro come team software e scritto codice più velocemente di quanto Lean riuscisse a verificarlo.

Questi dati provengono dal resoconto di Axiom; l’annuncio non include una revisione indipendente della formalizzazione. Al 28 ottobre, il post aveva circa 6.200 «Mi piace» su X.