Una dimostrazione di 500 pagine che nessuno è riuscito a leggere fino in fondo
Immaginate che un matematico pubblichi, da un giorno all’altro, la dimostrazione di uno dei problemi più difficili del suo campo — e che, dodici anni dopo, nessuno sia ancora in grado di dire se sia vera o falsa. È esattamente ciò che accade dal 2012 con la congettura abc, e forse è il più grande scandalo silenzioso della storia della matematica moderna. Per porvi fine, alcuni ricercatori hanno deciso di affidare il verdetto a una macchina.
La congettura abc: un problema dall’apparenza semplice, di profondità abissale
Prima di entrare nel vivo, gettiamo le basi. La congettura abc è un enunciato sui numeri interi, formulato negli anni Ottanta dai matematici Joseph Oesterlé e David Masser. La sua idea centrale si può riassumere così: se tre numeri interi a, b e c soddisfano l’equazione a + b = c, allora i fattori primi che compongono questi tre numeri non possono essere tutti molto piccoli contemporaneamente. In altre parole, una semplice somma fra due numeri interi vincola la struttura profonda dei loro divisori.
Formulata così, questa congettura può sembrare innocua, ma le sue implicazioni sono considerevoli: se fosse dimostrata, comporterebbe automaticamente la dimostrazione di decine di altri importanti teoremi della teoria dei numeri — il ramo della matematica che studia le proprietà dei numeri interi. L’ultimo teorema di Fermat, per esempio, ne discenderebbe quasi come un corollario. La congettura abc è dunque una sorta di chiave di volta: convalidarla significa aprire decine di porte in un colpo solo.
Mochizuki, il solitario di Kyoto
Nell’agosto 2012, Shinichi Mochizuki, professore all’Università di Kyoto, pubblicò sul proprio sito quattro articoli per un totale di oltre 500 pagine. Vi annunciava di aver dimostrato la congettura abc. Ma la dimostrazione non assomiglia a nulla di noto: si fonda su una teoria interamente nuova, che Mochizuki sviluppò da solo nell’arco di un decennio e che chiama teoria degli spazi di Teichmüller inter-universali — o IUT per gli amici.
Il problema? Questa teoria inventa i propri oggetti matematici, le proprie notazioni, le proprie regole del gioco. Per comprendere la dimostrazione, bisogna prima imparare una lingua che nessun altro ha mai parlato. Fra i matematici più brillanti del mondo, molti ci hanno provato. Molti hanno rinunciato dopo settimane o mesi di sforzi. Peter Scholze e Jakob Stix, due giganti della teoria dei numeri, affermarono infine nel 2018 di aver individuato una falla precisa nell’argomentazione — un passaggio chiave del ragionamento che, secondo loro, non regge.
« Non comprendiamo perché questo passaggio dovrebbe funzionare e non crediamo che funzioni. » — Peter Scholze e Jakob Stix, 2018
—
Mochizuki, dal canto suo, ha sostenuto che i suoi critici semplicemente non avevano compreso la sua teoria. Ha risposto a lungo, punto per punto, senza mai ammettere il minimo errore. E a quel punto il dialogo si è fermato. Si sono formati due schieramenti: quelli che ritengono corretta la dimostrazione, soprattutto stretti collaboratori di Mochizuki in Giappone, e quelli che la giudicano piena di falle. Il resto della comunità, la grande maggioranza, ha semplicemente rinunciato a decidere.
Perché una dimostrazione può restare controversa per dieci anni
Questo caso illustra un limite profondo del sistema di convalida della matematica. In linea di principio, una dimostrazione matematica è corretta oppure scorretta — non esistono zone grigie. In pratica, però, la convalida si basa sulla peer review, cioè sulla revisione tra pari: altri esperti del settore verificano ogni passaggio del ragionamento. Questo sistema funziona molto bene quando una dimostrazione si inscrive in un linguaggio condiviso. Crolla quando la dimostrazione reinventa quel linguaggio da cima a fondo.
Nessuno viene pagato per dedicare sei mesi a imparare un’intera teoria solo per verificarne la coerenza. I matematici hanno corsi da tenere, articoli da pubblicare, carriere da costruire. Esaminare la dimostrazione di Mochizuki rappresenta un investimento colossale, dal ritorno incerto. Risultato: la dimostrazione è stata sì pubblicata su una rivista — le Publications of the Research Institute for Mathematical Sciences di Kyoto, di cui Mochizuki è egli stesso caporedattore, circostanza che ha suscitato critiche per conflitto d’interessi — ma senza mai ottenere la convalida informale della comunità internazionale.
Il computer come arbitro di ultima istanza
È in questo contesto di totale stallo che emerge un nuovo approccio: la verifica formale assistita dal computer. Il principio è semplice. Software specializzati — chiamati proof assistants, o assistenti di prova — permettono di tradurre una dimostrazione matematica in un linguaggio formale che la macchina può verificare passaggio per passaggio, meccanicamente, senza stanchezza né pregiudizi. Se un passaggio non regge, il computer lo rileva.
Alcuni ricercatori hanno intrapreso la formalizzazione di parti fondamentali della teoria IUT in uno di questi assistenti. L’obiettivo è preciso: verificare l’esatto passaggio contestato da Scholze e Stix. Se il computer conferma la falla, il dibattito è chiuso. Se invece convalida il passaggio, costringerà la comunità a riconsiderare le proprie obiezioni.
Non è un’impresa banale. Formalizzare matematica avanzata in un assistente di prova richiede un lavoro considerevole — talvolta anni per poche pagine. Ma forse è l’unico modo per uscire da un’impasse che gli esseri umani, da soli, non sono riusciti a risolvere.
Le lezioni di uno scandalo matematico
Al di là del caso Mochizuki, questa vicenda pone interrogativi che vanno ben oltre un solo uomo o una sola congettura. Come dovrebbe trattare la comunità matematica le teorie radicalmente nuove, quelle che richiedono anni di apprendimento prima ancora di poter essere valutate? Chi deve sostenere il costo della verifica? E se nessuno lo fa, una dimostrazione non letta è davvero una dimostrazione?
La diffusione degli assistenti di prova apre una prospettiva concreta. La matematica formalizzata è verificabile da chiunque disponga del software adatto. Non dipende più dalla buona volontà di una manciata di esperti oberati. Alcuni ricercatori sostengono già che le grandi dimostrazioni debbano essere sistematicamente accompagnate dalla loro versione formale. Sarebbe una rivoluzione nel modo in cui la matematica viene fatta e trasmessa.
Nel frattempo, il verdetto della macchina è atteso con un’impazienza venata d’inquietudine. Perché se il computer confermerà la falla, bisognerà trarre una conclusione scomoda: per oltre un decennio, la comunità matematica mondiale è stata incapace di convalidare o invalidare uno dei propri presunti risultati più importanti. E questa è una falla del sistema, non soltanto di una dimostrazione.
Concetti da ricordare
Per i matematici
La congettura abc si formula con precisione mediante la nozione di radicale di un numero intero. Per un intero n, si definisce rad(n) come il prodotto di tutti i fattori primi distinti di n — senza tenere conto delle loro molteplicità. Per esempio, rad(12) = rad(2² × 3) = 2 × 3 = 6. La congettura afferma allora che, per ogni numero reale ε > 0, esiste soltanto un numero finito di terne di numeri interi (a, b, c) coprimi a due a due, che soddisfano a + b = c e tali che c > rad(abc)1+ε. In altre parole, i casi in cui c è «molto più grande» del radicale del prodotto abc sono estremamente rari. Questa formulazione esprime l’idea che la presenza di potenze elevate nella fattorizzazione in primi di una somma sia un’anomalia, non la norma.
