Per la prima volta, una intelligenza artificiale non si è limitata ad assistere i ricercatori, ma ha prodotto dimostrazioni formali complete di teoremi che erano rimasti irrisolti per anni. Il sistema si chiama AxiomProver ed è stato sviluppato dalla startup Axiom: non un chatbot evoluto, ma un motore capace di ragionare nel linguaggio matematico formale e verificare ogni passaggio logico.
La svolta è emersa quando una congettura di geometria algebrica, rimasta sospesa per cinque anni, è stata finalmente dimostrata. I matematici Dawei Chen e Quentin Gendron avevano trasformato il loro teorema in una semplice ipotesi dopo essersi bloccati su una formula di teoria dei numeri che nessuno riusciva a dimostrare. La soluzione è arrivata grazie all’intervento di Ken Ono, che ha utilizzato AxiomProver per generare una dimostrazione completa e formalmente verificata.
Non un chatbot, ma un sistema formale
A differenza di strumenti come ChatGPT, che producono risposte linguisticamente coerenti ma non certificate dal punto di vista logico, AxiomProver lavora nel linguaggio Lean, uno standard per la verifica matematica formale. Questo significa che ogni riga della dimostrazione viene controllata automaticamente, eliminando ambiguità e scorciatoie concettuali.
Nel caso della congettura di Chen e Gendron, l’AI matematica ha individuato un collegamento con fenomeni numerici studiati nel XIX secolo, costruendo un percorso che nessun ricercatore aveva esplorato. La dimostrazione è stata poi pubblicata su arXiv, confermando la validità scientifica del risultato. Ma l’aspetto più rilevante non è solo la soluzione in sé: è il fatto che la macchina abbia costruito autonomamente una catena logica rigorosa, entrando in un territorio considerato per decenni esclusivamente umano.
Nuove dimostrazioni e legami con la storia della matematica
La congettura risolta non è un episodio isolato. Secondo quanto dichiarato da Axiom, il sistema ha prodotto altre dimostrazioni relative a problemi rimasti aperti per anni, inclusa la cosiddetta congettura di Fel sulle “sizigie”, strutture complesse dell’algebra moderna.
In alcuni casi, l’AI ha richiamato formule che comparivano nei taccuini di Srinivasa Ramanujan, mostrando connessioni tra intuizioni storiche e strumenti contemporanei. Un’altra dimostrazione si basa su metodi sviluppati per l’Ultimo teorema di Fermat, uno dei problemi più celebri della matematica moderna, suggerendo che l’AI sia capace di combinare conoscenze lontane nel tempo in modo originale. Questi risultati indicano che non siamo di fronte a un semplice supporto computazionale, ma a una forma di collaborazione cognitiva tra uomo e macchina.
Cosa cambia per i matematici
Secondo Carina Hong, la matematica rappresenta il banco di prova ideale per l’intelligenza artificiale, perché richiede rigore assoluto e verificabilità totale. Se un sistema riesce a operare in questo ambito, può essere applicato anche alla verifica del software, alla sicurezza informatica e ad altri settori dove l’errore non è ammesso.
Anche Scott Kominers ha sottolineato non solo la validità tecnica delle dimostrazioni, ma la loro eleganza strutturale. Un riconoscimento che suggerisce come l’AI non si limiti a “forzare” una soluzione, ma possa proporre percorsi matematicamente raffinati. Il cambiamento più profondo riguarda il ruolo dei ricercatori. Con strumenti come AxiomProver, il matematico non viene sostituito, ma affiancato da un sistema capace di esplorare rapidamente combinazioni logiche che richiederebbero anni di lavoro manuale. La ricerca matematica potrebbe così accelerare, spostando l’attenzione dall’esecuzione delle verifiche alla formulazione di nuove domande.
Se fino a ieri la dimostrazione era considerata il punto culminante del ragionamento umano, oggi l’intelligenza artificiale entra in quel processo come partner attivo. E il fatto che alcune congetture ferme da anni siano state risolte in questo modo suggerisce che la frontiera tra capacità umana e capacità algoritmica sia destinata a diventare sempre più sottile.
