Lo sviluppatore ha utilizzato l'intelligenza artificiale per dimostrare l'ipotesi di Conway

Lo sviluppatore Dan Abramov ha presentato una prova formale della 50enne congettura di Conway sui numeri surreali, utilizzando le capacità dei modelli generativi per lavorare con il linguaggio di programmazione Lean. Il processo ha richiesto circa un mese di lavoro continuo con gli strumenti AI per la generazione e la verifica di affermazioni matematiche.

La congettura di Conway, relativa alla precisazione delle proprietà dei numeri surreali, era rimasta irrisolta per mezzo secolo. Nel corso del lavoro, l'autore ha utilizzato LLM per scrivere codice su Lean, che formalizza gli oggetti matematici e le transizioni logiche. Il risultato finale è un set di script che passano la compilazione nell'ambiente Lean, confermando la correttezza delle affermazioni dedotte all'interno dell'assiomatica data.

Nonostante la compilazione del codice sia stata completata con successo, la prova attende attualmente una verifica indipendente da parte della comunità matematica professionale. L'utilizzo di AI ha permesso di automatizzare le fasi di routine della formalizzazione, che normalmente richiedono notevoli quantità di tempo quando vengono inserite manualmente nel sistema di prova.

Questo caso dimostra il potenziale dell'integrazione di LLM nel campo della verifica formale delle teoremi matematiche. In precedenza, compiti simili richiedevano una profonda conoscenza della sintassi di Lean e una lunga pratica, tuttavia l'applicazione di AI riduce la soglia di ingresso per la formalizzazione di costruzioni matematiche complesse. Un ulteriore sviluppo degli strumenti basati su Lean potrebbe accelerare la verifica di ipotesi che in precedenza erano considerate troppo faticose per l'elaborazione manuale.