Pin It

Fermi tutti: c’è qualcosa che non funziona in una delle più spettacolari e famose conquiste matematiche del XX secolo, la dimostrazione dell’Ultimo Teorema di Fermat? E perché ce ne accorgiamo solo adesso, dopo 30 anni?

Un gruppo di ricercatori dell’Imperial College London ha di recente avviato un ambizioso progetto che mira a formalizzare la dimostrazione dell’Ultimo Teorema di Fermat, che afferma che non esistono soluzioni intere positive dell’equazione

\(a^n+b^n=c^n\)

se \(n>2\).
Si tratta del famigerato teorema di Pierre de Fermat nel 1637, di cui però il grande matematico francese non fornì la dimostrazione, limitandosi ad annotare l’equazione su una pagina di una copia dell’Arithmetica di Diofanto e poi aggiungendo “Ho una meravigliosa dimostrazione di questo teorema, che non entra nello stretto margine della pagina”.

Solo nel 1994, quindi oltre tre secoli di tentativi dopo, la Congettura di Fermat è stata dimostrata – venendo promossa a “Teorema” – da Andrew Wiles, con un complicatissimo lavoro di 200 pagine (poi ridotte a 130) che è considerato spesso al di là della comprensione della maggior parte delle persone non specializzate in teoria dei numeri.

Quando ci si trova di fronte a stesure così lunghe e complesse, ai matematici moderni viene in soccorso il computer. Il “proof assistant” è un software che aiuta (anche) a verificare dimostrazioni formali di teoremi quando per un essere umano potrebbe essere estremamente difficile procedere manualmente. Utilizzando sistemi di logica formale, il proof assistant garantisce che ogni passaggio sia corretto, rispettando precise regole matematiche.

Uno dei proof assistant più usati è Lean ed è stato proprio Lean che ha messo alla prova la dimostrazione dell’Ultimo Teorema di Fermat – non quella vecchia degli anni ’90 ma quella generale e semplificata a cui, nel corso degli anni, ha contribuito il lavoro di molti matematici come Diamond/Fujiwara, Kisin, Taylor e tanti altri.

Un concetto utilizzato in quest’ultima versione della dimostrazione (e non presente in quella di Wiles) è la coomologia cristallina, una teoria sviluppata negli anni ’60 e ’70 a Parigi da Pierre Berthelot seguendo le idee di Alexander Grothendieck. La teoria delle “strutture di potenza divisa” è stata sviluppata negli anni ’60 in una serie di articoli del matematico francese Norbert Roby. Sottoponendo la dimostrazione a Lean, Antoine Chambert-Loir dell’Università Paris Cité, coinvolto nel progetto dell’Imperial College, ha visto che il software rilevava che un lemma chiave nel lavoro di Roby poteva essere errato. Nel lavoro di Roby “Les algebres à puissances divisées“, pubblicato in Bulletin des Sciences Mathématiques, 2a serie, 89, 1965, pp. 75-91, il Lemma 8 (a pagina 86) sembrava infatti essere falso e non era banale il modo di correggerne la dimostrazione.

Si trattava di un difetto che, se trascurato, avrebbe potuto avere severi effetti collaterali al di là di quella dimostrazione del Teorema di Fermat, vanificando enormi quantità di lavori legati alla coomologia cristallina. Tuttavia, quello che Lean aveva provato, in senso stretto, non era che il lemma non fosse valido ma che la sua dimostrazione nascondeva un errore – che avrebbe potuto essere semplicemente sistemato.

I matematici non si sono fatti prendere dal panico perché la coomologia cristallina è ampiamente utilizzata da circa 50 anni e, se ci fosse stato un problema fondante, sarebbe certamente dovuto già venire alla luce molto tempo fa. Grazie alla “denuncia” di Lean, Chambert-Loir ha scoperto che Roby poteva aver dimenticato un simbolo tra una riga e l’altra: successivamente, con la collaborazione di altri matematici, è stato però fatto notare che la conclusione a cui portava quel lemma (ossia che “l’algebra universale delle potenze divise di un modulo ha potenze divise”) poteva essere raggiunta anche in un altro modo, che era presente nell’appendice di un libro di Berthelot-Ogus sulla coomologia cristallina. Insomma: l’Ultimo Teorema di Fermat è salvo.

 

Pin It
This website uses the awesome plugin.