Els matemàtics fa dècades que mantenen llistes de problemes oberts, és a dir, preguntes sense resposta coneguda. Una de les més famoses és la de Paul Erdős, amb centenars d'enunciats. Fins ara, els sistemes d'IA havien aportat demostracions soltes, sovint difícils de comprovar i no sempre revisades per cap revista.
Google DeepMind ha publicat a *Science* (DOI 10.1126/science.aej2213) els resultats d'AlphaProof Nexus, un sistema que escriu i corregeix demostracions en Lean, un llenguatge formal que un programa pot verificar pas a pas. Segons la crònica de The Decoder, el sistema fa servir Gemini 3.1 Pro i pot recórrer a AlphaProof per als trams més difícils. Ha resolt nou dels 353 problemes oberts d'Erdős que es va proposar, dos dels quals feia 56 anys que ningú no els resolia. També ha demostrat 44 conjectures de l'enciclopèdia de successions OEIS, ha resolt una pregunta oberta de geometria algèbrica i ha millorat una fita coneguda en optimització.
La novetat no és només la xifra, sinó el mètode: Lean comprova cada esborrany després de cada canvi i els seus missatges d'error guien l'intent següent, de manera que una demostració acceptada no depèn de la paraula del model. DeepMind explica que va compartir les solucions en línia abans que sortís l'article i que el sistema va resoldre els nou problemes d'Erdős fins i tot sense AlphaProof. El contrast és evident amb altres laboratoris, que han penjat centenars de demostracions generades per IA sense enviar-les a cap revista, cosa que ha portat un grup de matemàtics encapçalat per Terence Tao a demanar un boicot.
Convé no inflar-ne l'abast: nou problemes sobre 353 són una part petita de la llista, i aquest article no detalla les limitacions del sistema. Tampoc no hem pogut consultar el text de l'article a *Science* directament, i la xifra i els detalls procedeixen de la crònica de The Decoder. El que sí que és nou és que una demostració feta per IA arriba a una revista de primer nivell amb una verificació formal al darrere.