Nuevo paradigma: La inteligencia artificial ha resuelto cuatro problemas matemáticos que llevaban años sin respuesta, marcando un hito en la colaboración humano-máquina.
Hace cinco años, los matemáticos Dawei Chen y Quentin Gendron intentaban demostrar un teorema en geometría algebraica relacionado con diferenciales. Su argumento dependía de una fórmula numérica que no lograban resolver, por lo que publicaron su trabajo como una conjetura. El obstáculo parecía insuperable hasta que Chen recurrió a Ken Ono, matemático que ahora trabaja en Axiom, una startup de IA cofundada por su exalumna Carina Hong.
Ono utilizó AxiomProver, la herramienta de IA de la empresa, para resolver el problema en cuestión de horas. La solución conectó el teorema con un fenómeno numérico del siglo XIX y generó una prueba autoverificada. «Lo que AxiomProver encontró fue algo que todos los humanos habían pasado por alto», explicó Ono a WIRED. La demostración, ya publicada en arXiv, confirmó la conjetura de Chen-Gendron.
La IA de Axiom ha resuelto tres problemas matemáticos más en las últimas semanas, demostrando avances significativos en el campo.
Soluciones en tiempo récord
AxiomProver no ha resuelto los problemas más famosos de las matemáticas, pero sí ha respondido preguntas que llevaban años sin solución. Estas pruebas reflejan cómo la IA avanza rápidamente en matemáticas, un área donde otros investigadores también han comenzado a usarla para explorar nuevas ideas.
Las aplicaciones de esta tecnología van más allá de las matemáticas puras. Podría usarse para desarrollar software más resistente a ciberataques, verificando que el código sea demostrablemente seguro. «Las matemáticas son el gran campo de pruebas de la realidad», afirma Hong, CEO de Axiom. «Hay muchos casos de uso con gran valor comercial».
El sistema de Axiom combina grandes modelos de lenguaje con AxiomProver, un motor de IA entrenado para razonar matemáticamente y generar soluciones verificables. En 2024, Google presentó un sistema similar llamado AlphaProof, pero Hong destaca que AxiomSolver incorpora técnicas más avanzadas.
Pruebas que sorprenden a los expertos
AxiomProver no solo resuelve problemas, sino que lo hace utilizando un lenguaje matemático especializado llamado Lean, que le permite verificar sus propias pruebas. Esto le da una ventaja sobre los modelos tradicionales de IA, que se limitan a buscar patrones en datos existentes.
Una de las demostraciones más destacadas resolvió la conjetura de Fel, relacionada con las «sizigias» en álgebra. Lo sorprendente es que la solución involucró fórmulas descubiertas por el matemático indio Srinivasa Ramanujan hace más de un siglo. «No se trata solo de resolver un problema, sino de la elegancia de las matemáticas que produce», comentó Scott Kominers, profesor de Harvard.
Otras dos pruebas generadas por la IA se basan en modelos probabilísticos de teoría de números y en herramientas desarrolladas para resolver el último teorema de Fermat, uno de los desafíos más famosos de la historia.
Ken Ono espera que AxiomProver no solo ayude a los matemáticos, sino que también revele cómo surgen los grandes descubrimientos.
Chen, quien vio cómo la IA resolvía su propia conjetura, compara el impacto de estas herramientas con el de la calculadora: «Los matemáticos no olvidaron las tablas de multiplicar tras su invención. La IA será un socio inteligente que ampliará los horizontes de la investigación».
Ono añade: «Se trata de un nuevo paradigma para demostrar teoremas».
Lecturas relacionadas
- La paradoja de la IA en América Latina: ¿moldeará la tecnología o será moldeada por ella?
