Des de fa mesos, els laboratoris d'IA competeixen per demostrar que els seus models poden fer matemàtica nova i no només resoldre exercicis. Els problemes que va plantejar Paul Erdős, molts encara oberts, s'han convertit en un banc de proves habitual.
Un equip de Google DeepMind, amb George Tsoukalas com a primer firmant, publica a «Science» l'article «Advancing mathematics research with AI-driven formal proof search», sobre un sistema anomenat AlphaProof Nexus. Hi treballen diversos agents d'IA que busquen demostracions i reben com a resposta el compilador de Lean, un llenguatge que verifica cada pas de manera automàtica. Una versió més avançada coordina subagents amb un algorisme evolutiu i fa servir AlphaProof com a eina especialitzada. Segons la nota de la revista, el sistema va resoldre 9 dels 353 problemes d'Erdős que va intentar, dos dels quals feia més de cinquanta anys que estaven oberts, i 44 de les 492 conjectures obertes de l'Enciclopèdia en línia de successions de nombres enters. També hi ha resultats en geometria algebraica, optimització, òptica quàntica i teoria de grafs.
El valor del treball és que les demostracions no cal creure-les: Lean les comprova. Això respon a un dels grans problemes dels models de llenguatge, que poden cometre errors lògics subtils. Jeremy Avigad, de la Carnegie Mellon, i Matthew Ballard, de la Universitat de Carolina del Sud, hi signen un comentari a la mateixa revista, on destaquen que fins i tot els intents fallits poden ajudar els matemàtics a entendre millor un problema.
Els límits són clars: l'èxit ha estat d'un 2,5% en els problemes d'Erdős i d'un 9% en les conjectures de successions, i el sistema només ataca problemes escollits. Cal que la comunitat matemàtica en confirmi l'abast més enllà de la revisió de la revista.