Il matematico Andrew Wiles ha impiegato otto anni di isolamento per dimostrare l’Ultimo Teorema di Fermat, consegnando al mondo nel 1994 un manoscritto di oltre cento pagine denso di passaggi logici complessi. A trent’anni di distanza, un gruppo internazionale di ricerca guidato dal matematico Kevin Buzzard dell’Imperial College London ha avviato la traduzione di quella storica dimostrazione in un codice informatico verificabile automaticamente attraverso il software Lean.L’iniziativa punta a convertire l’intero impianto teorico del teorema — enunciato da Pierre de Fermat nel 1637 e rimasto per secoli il rompicapo più celebre della matematica — in una sequenza rigorosa che non lasci spazio ad alcun margine di errore umano.
La prova originale di Wiles non si limitava a risolvere la nota equazione, ma univa due branche distinte della disciplina: le forme modulari e le curve ellittiche. Per rendere il testo comprensibile all’assistente di prova digitale, i ricercatori stanno formalizzando la congettura di Taniyama-Shimura-Weil, il vero pilastro concettuale su cui poggia l’intera architettura della dimostrazione.Il progetto richiede di smontare ogni passaggio in assiomi elementari, mappando dettagliatamente definizioni che i matematici in carne e ossa danno spesso per scontate. Questo lavoro di codifica ha già portato alla digitalizzazione di interi capitoli della teoria dei numeri moderna, creando una biblioteca di strumenti logici a disposizione di futuri studiosi. L’obiettivo va oltre la semplice conferma del risultato di Wiles: la formalizzazione digitale apre la strada a un nuovo modo di validare le teorie più complesse, riducendo il rischio che sviste o imprecisioni sfuggano ai revisori umani.
https://www.zmescience.com/science/news-science/fermats-last-theorem-formalized
