Un modello sperimentale di Claude, l'intelligenza artificiale messa a punto da Anthropic, ha portato a termine la traduzione in codice informatico della dimostrazione dell'Ultimo Teorema di Fermat. L'operazione ha richiesto appena undici giorni, un lasso di tempo che, secondo le stime di un progetto di ricerca guidato dal matematico Kevin Buzzard, avrebbe impegnato gli esperti per circa un decennio.
Per formalizzare il ragionamento, il sistema ha utilizzato Lean, un linguaggio progettato specificamente per la rappresentazione rigorosa delle dimostrazioni matematiche, generando circa 13 milioni di righe di codice e oltre 30.300 teoremi intermedi. Il traguardo giunge dopo alcuni tentativi precedenti naufragati a causa dell'interruzione della collaborazione tra gli agenti coinvolti nel progetto.
Il teorema, formulato nel 1637 e legato concettualmente al teorema di Pitagora, era stato risolto negli anni '90 da Andrew Wiles con il supporto di Richard Taylor. La conversione operata da Claude rappresenta la prima traduzione integrale di questa complessa costruzione in un formato verificabile elettronicamente.
Permangono tuttavia ostacoli tecnici: il codice prodotto non è attualmente compatibile con MathLib, la libreria standard utilizzata dalla comunità accademica per la verifica formale, impedendone l'integrazione immediata nei flussi di lavoro scientifici.
