Les demostracions matemàtiques es comproven tradicionalment llegint-les, i els errors de vegades passen anys sense que ningú els vegi. Una alternativa és la verificació formal: reescriure cada demostració en un llenguatge de programació com Lean, de manera que un programa, l'assistent de demostració, en revisi la lògica línia per línia. És una feina lenta i pesada, i hi ha camps sencers, com la geometria algebraica, on gairebé no hi havia material verificat.
L'empresa emergent nord-americana Axiom Math, valorada en 1.600 milions de dòlars, va anunciar dimecres que una flota d'agents d'IA ha verificat formalment el Stacks Project, una obra de consulta oberta de geometria algebraica que el matemàtic Johan de Jong, de la Universitat de Colúmbia, va començar el 2005. Segons l'empresa, els agents han traduït unes 7.654 pàgines a uns 16 milions de línies de codi Lean comprovades per l'ordinador, i han mantingut la coherència entre els milers de teoremes i definicions que depenen els uns dels altres. Els agents treballaven en paral·lel i triaven ells mateixos les tasques, amb models especialitzats en matemàtiques entrenats per l'empresa i, al principi, la guia d'un expert en Lean de la casa.
L'interès va més enllà d'aquesta obra: cada resultat verificat es pot reutilitzar com a peça per construir-ne d'altres, i la mateixa tècnica serveix per comprovar programari, ara que els agents d'IA escriuen cada vegada més codi. El matemàtic Terence Tao, medalla Fields, ho resumeix a TechCrunch: «Com més demostracions formalitzades tens, més demostracions formalitzades pots fer». La directora executiva de l'empresa, Carina Hong, ha desafiat les altres empreses de programació a treballar a aquesta escala.
És un anunci d'una empresa, no un treball revisat per altres matemàtics, i el resultat es pot consultar en una web de demostració. Una verificació formal garanteix que les demostracions són correctes tal com s'han escrit en Lean, però no que la traducció reprodueixi fidelment el que deien els enunciats originals, i fins i tot les comprovacions per ordinador poden deixar escapar errors, com recorda el mateix article.