Il famoso problema posto nel 1637 da Pierre de Fermat ha tormentato i matematici per secoli e afferma che non esistono numeri interi positivi \(a\), \(b\) e \(c\) che soddisfino l’equazione \(a^n+b^n=c^n\) per ogni \(n\) intero positivo maggiore di 2. A Wiles e Taylor sono serviti sette anni di lavoro e un anno aggiuntivo per la correzione di un errore emerso nella prima versione.
Una dimostrazione matematica scritta su carta consiste in una lunga catena di ragionamenti, e un solo anello difettoso può far crollare tutto. I matematici da qualche anno traducono le dimostrazioni in Lean, un linguaggio di programmazione fatto apposta per la matematica in cui ogni passaggio viene scritto in modo che un computer possa controllarlo con sicurezza, senza possibilità di sviste. Se il computer arriva fino in fondo senza obiezioni, la dimostrazione è certificata. Tutta la matematica che è stata già tradotta in Lean è raccolta in Mathlib, una sorta di grande biblioteca condivisa online, che attualmente ospita circa 2 milioni di righe di codice che chiunque può consultare e usare per costruire nuove dimostrazioni senza dover ripartire da zero.
Il matematico Kevin Buzzard, dell’Imperial College di Londra, aveva avviato un progetto per tradurre in Lean le cento pagine di Wiles, e stimava i tempi di lavoro in circa 5 anni. Anthropic ha invece realizzato l’impresa con il suo modello Claude che ha operato incessantemente per 11 giorni, dopo aver diviso il compito tra tanti agenti che lavoravano in parallelo su pezzi diversi del problema.
