// SMARTWORLD — INTELLIGENZA ARTIFICIALE
Claude ha formalizzato il Teorema di Fermat in codice in 11 giorni
Una versione sperimentale di Claude, il modello di intelligenza artificiale sviluppato da Anthropic, ha completato la traduzione in codice informatico della dimostrazione del Teorema di Fermat. Lo ha annunciato la stessa azienda sul proprio blog ufficiale: l'operazione ha richiesto undici giorni, durante i quali il sistema ha prodotto circa 13 milioni di righe nel linguaggio Lean.
Lean è uno strumento pensato per rappresentare i ragionamenti matematici in una forma che un computer possa verificare in modo rigoroso. Il risultato è particolarmente significativo perché lo stesso obiettivo era già al centro di un progetto umano guidato dal matematico Kevin Buzzard, la cui stima di completamento era di circa dieci anni di lavoro.
Il Teorema di Fermat, formulato nel 1637 e noto anche come Ultimo Teorema di Fermat, è uno dei problemi più celebri della storia della matematica. Si basa su un'idea molto vicina a quella del Teorema di Pitagora, ma generalizzata in modo da risultare straordinariamente difficile da dimostrare.
La dimostrazione arrivò solo negli anni '90, grazie al matematico Andrew Wiles e al successivo contributo di Richard Taylor, attraverso una costruzione molto complessa. Claude ha ora tradotto questa dimostrazione in codice verificabile da un computer per la prima volta, elaborando e producendo circa 30.300 teoremi intermedi.
Il percorso non è stato lineare: il modello ha raggiunto il risultato dopo diversi tentativi falliti, perché gli agenti AI che lavoravano al progetto avevano smesso di collaborare tra loro dopo le fasi iniziali.
Al momento il materiale generato presenta una limitazione tecnica: il codice prodotto da Claude non può essere integrato nella libreria standard MathLib, il riferimento utilizzato dalla comunità accademica per questo tipo di formalizzazioni matematiche.