Maurizio Codogno, meglio noto in rete come .mau., racconta come lui vede la matematica, con la scusa di non doverla insegnare né crearne di nuova. AxiomProver non solo dimostra teoremi, ma dimostra formalmente la dimostrazione. Ma non basta ancora per fare il matematico.

A metà febbraio è apparsa sui siti specializzati la notizia che c’era un’IA “che risolve i problemi matematici che nemmeno gli esperti erano riusciti a decifrare”, come scrisse Wired. Quello che era successo era che due matematici che stavano lavorando nel campo della geometria algebrica si erano trovati davanti a una congettura che si basava su un risultato della teoria dei numeri che non riuscivano a dimostrare: poco dopo l’incontro con Ken Ono, matematico che lavora per la startup Axiom, costui ha usato il sistema AxiomProver per trovare che la proprietà richiesta era stata dimostrata nel XIX secolo; quindi ha dimostrato formalmente la congettura. Niente male, vero? Peccato che dopo questo exploit non si sia più sentito parlare di AxiomProver. Ho trovato solo questo altro risultato (parziale) che Ono ha postato qualche settimana fa. Una rivoluzione con il freno a mano tirato, si direbbe. Visto che dall’articolo di Wired non mi era chiaro di che si parlasse, sono andato alla ricerca del paper; non ci ho capito molto di più, non ho mai studiato geometria algebrica, ma perlomeno ho visto che il teorema di teoria dei numeri era un’estensione della legge di reciprocità quadratica che era stata dimostrata da un certo M. Jenkins nel 1866; uno di quei risultati che non finiscono nei libri ma come in questo caso possono spuntare fuori in un contesto totalmente diverso.

In tempi non sospetti ho già espresso i miei dubbi su Axiom, e quindi non mi ripeto pedissequamente. È però giusto aggiungere qualcosa su quanto di positivo hanno fatto. Innanzitutto Ken Ono non è l’ultimo arrivato in campo matematico, il che significa che il lavoro che Axiom sta facendo non è campato in aria. Poi sono rimasto favorevolmente impressionato da qualcosa che i veri matematici hanno snobbato, che cioè AxiomProver abbia risolto i 12 problemi Putnam 2025, dando una dimostrazione formale della correttezza delle risposte: il modulo Lean da questo punto di vista è fondamentale nella definizione del modello, perché permette al modulo IA di sparare a poco prezzo tante possibili “dimostrazioni” che poi vengono verificate autonomamente. Come dicevo, ho letto di molti che derubricavano il risultato a semplice applicazione di regole più o meno standard, dato che i problemi Putnam sono generalmente più semplici di quelli delle Olimpiadi della matematica; ma oggettivamente il riuscire a muoversi nello spazio delle probabilità di generazione di testo e trovare una soluzione dal mio punto di vista è rimarchevole.

Ma guardiamo un po’ meglio cosa succede. Anche la dimostrazione di una congettura di Leonid Fel, che è sicuramente il risultato più importante ottenuto fino ad oggi da AxiomProver, parte da un dato di fatto: gli autori ammettono che hanno scelto quel problema aperto perché ritenevano che fosse formalizzabile con le attuali capacità del repository Mathlib usato dal modulo Lean. Quello che è successo, insomma, è che AxiomProver ha risolto un problema nuovo, ma in un ambiente noto: ha insomma le capacità di un ottimo studente universitario che riesce a risolvere un problema che il suo relatore gli ha dato per la tesi, ma non inventa nuova matematica. Come scrisse William Thurston nel suo articolo del 1994 On Proof and Progress in Mathematics, dire che il progresso in matematica si ottiene solo dimostrando formalmente teoremi è riduttivo, e dà un’immagine davvero povera della matematica. Pensate all’ultimo teorema di Fermat, e alle tecniche che sono state ideate nei tre secoli abbondanti dopo la morte del Grande Dilettante per cercare di affrontare il problema. O più in piccolo pensate a tutti i tentativi che fece Conway prima di trovare la “regola perfetta” per il suo Life oppure alla congettura di Collatz, dove avere 3n − 1 oppure 5n + 1 come regola sgonfia immediatamente la struttura. Tutto questo non è alla portata di AxiomProver.

Ma c’è qualcosa di ancora più sottile che traspare da quanto ho appena scritto. Questo software non ha gusto. È un Mister Wolf, uno che risolve problemi, ma i problemi non li sa creare. Se preferite, potrebbe creare enunciati su enunciati formalmente veri, ma per nulla interessanti. In matematica non è solo importante sapere cosa è vero, ma anche il perché lo è; un bravo matematico parte da una stranezza che ha visto e la usa come punto di partenza per fare della nuova matematica. AxiomProver non ha nulla di tutto questo: può solo prendere quanto i matematici gli danno in pasto, senza scegliere nulla. Non so se possiamo associare il gusto alla coscienza: ma sicuramente c’è ancora moltissima strada da fare per avere un software che fa matematica, e non la risolve solo.

Guarda la pagina di questa rubrica

Maurizio Codogno

Maurizio Codogno, noto online come .mau., è nato a Torino nel 1963, e si è laureato in matematica presso la Scuola Normale Superiore di Pisa e successivamente in informatica a Torino. Autore di numerosi libri di divulgazione scientifica, tra cui “Matematica in pausa caffè” e “Chiamatemi Pi Greco”, ha il suo blog “Notiziole di .mau.” dall’inizio del millennio ed è stato curatore della collana di libri Matematica di Gazzetta dello Sport e Corriere della Sera.