Cinque anni fa i matematici Dawei Chen e Quentin Gendron stavano cercando di districarsi in un angolo particolarmente complesso della geometria algebrica, che coinvolge l’uso dei differenziali, strumenti del calcolo utilizzati per misurare le distanze lungo superfici curve. Mentre lavoravano a un teorema, si sono imbattuti in un ostacolo inatteso: il loro ragionamento dipendeva da una strana formula della teoria dei numeri, che non riuscivano né a risolvere né a giustificare.Alla fine i due hanno deciso di presentare il loro lavoro sotto forma di congettura, anziché di teorema.
Di recente Chen ha passato ore a dare in pasto prompt a ChatGPT, nella speranza che l’AI riuscisse a individuare una soluzione al problema ancora irrisolto, senza però ottenere risultati. Poi, durante un ricevimento a una conferenza di matematica a Washington di gennaio, il matematico ha incontrato Ken Ono, un collega molto noto che aveva da poco lasciato il suo incarico all’Università della Virginia per andare a lavorare ad Axiom, una startup di intelligenza artificiale cofondata da Carina Hong, sua ex allieva.
Cos’è e come funziona AxiomProver
Chen ha raccontato il suo problema a Ono, che la mattina seguente si è presentato con una dimostrazione ottenuta grazie ad AxiomProver, l’AI specializzata in problemi matematici della sua startup. “A quel punto ogni cosa è andata al suo posto in modo naturale”, racconta Chen, che ha collaborato con Axiom alla stesura della dimostrazione, ora pubblicata su arXiv, un archivio pubblico di articoli accademici.
Lo strumento di Axiom è riuscito a trovare un collegamento tra il problema e un fenomeno numerico studiato per la prima volta nel diciannovesimo secolo. In seguito, ha elaborato una dimostrazione e l’ha anche verificata. “AxiomProver ha trovato qualcosa che era sfuggito a tutti gli esseri umani”, spiega Ono a Wired.
Axiom sostiene che la dimostrazione sia una delle soluzioni a problemi matematici irrisolti che il suo sistema ha individuato nelle ultime settimane. L’AI non ha ancora risolto nessuno dei problemi più celebri (o più remunerativi) della matematica, ma ha trovato risposte a quesiti che da anni mettevano in difficoltà gli esperti di diversi settori.
