En el ámbito de la matemática, desafíos complejos han persistido durante décadas, frustrando a muchos expertos. Recientemente, dos matemáticos, Dawei Chen y Quentin Gendron, se enfrentaron a un dilema en el campo de la geometría algebraica. Mientras investigaban un teorema, encontraron un obstáculo inesperado relacionado con una fórmula de la teoría de números que no pudieron resolver. En lugar de presentar su hipótesis como un teorema, decidieron publicarla como una conjetura.
Después de varios intentos fallidos, Chen recurrió a ChatGPT en busca de sugerencias, pero no logró encontrar la solución. Sin embargo, todo cambió en un evento de matemáticas en Washington D.C, donde conoció a Ken Ono, un destacado matemático que recientemente se unió a Axiom, una startup de inteligencia artificial cofundada por Carina Hong, una de sus alumnas. Chen le expuso su problema y, al día siguiente, Ono le presentó una solución generada por el sistema de inteligencia artificial de Axiom, conocido como AxiomProver.
El impacto de AxiomProver en la resolución de problemas matemáticos
AxiomProver logró descubrir una conexión entre la conjetura de Chen-Gendron y un fenómeno numérico investigado desde el siglo XIX. Esta herramienta no solo propuso una prueba, sino que también la verificó por sí misma, marcando un avance significativo en el uso de la inteligencia artificial en matemáticas. Según Ono, «lo que AxiomProver encontró fue algo que todos los humanos habían pasado por alto».
Desarrollo de soluciones innovadoras
Axiom ha reportado que su sistema ha generado varias soluciones a problemas matemáticos previamente sin resolver en las últimas semanas. Aunque todavía no ha abordado los problemas más conocidos del ámbito matemático, ha proporcionado respuestas a cuestiones que han desconcertado a expertos durante años. Estas pruebas son testimonio del crecimiento constante de las capacidades matemáticas de la inteligencia artificial.
Aparte de su aplicación en matemáticas, las técnicas desarrolladas por Axiom podrían tener un impacto significativo en otros campos, como la ciberseguridad.
Por ejemplo, las metodologías empleadas podrían utilizarse para crear software más resistente a ciertos tipos de ataques cibernéticos, asegurando que el código sea fiable y comprobado.
El futuro de la inteligencia artificial en matemáticas
La visión de Carina Hong, CEO de Axiom, es que “las matemáticas son realmente el gran campo de pruebas y sandbox para la realidad”. Se cree que existen numerosas aplicaciones comerciales de alto valor que pueden surgir de estos avances. Axiom combina grandes modelos de lenguaje con su sistema propietario, AxiomProver, diseñado para razonar a través de problemas matemáticos y alcanzar soluciones verificables.
Avances comparativos con otros sistemas
En, Google presentó una idea similar con un sistema llamado AlphaProof. Sin embargo, Hong sostiene que AxiomSolver incluye varias innovaciones y técnicas más actuales. La prueba generada por Axiom para la conjetura de Chen-Gendron ilustra cómo la inteligencia artificial puede asistir de manera significativa a los matemáticos profesionales. Ono afirma, “este es un nuevo paradigma para probar teoremas”.
AxiomProver no solo busca en la literatura existente, sino que también verifica pruebas a través de un lenguaje matemático especializado llamado Lean. Esto le permite desarrollar formas genuinamente novedosas de abordar problemas.
Un ejemplo de las nuevas pruebas generadas por AxiomProver es la resolución de la Conjetura de Fel, que se centra en los syzygies, expresiones matemáticas donde los números se alinean en álgebra. Lo notable es que esta conjetura involucra fórmulas encontradas en los cuadernos del legendario matemático indio Srinivasa Ramanujan hace más de un siglo. En este caso, AxiomProver no solo completó una pieza faltante del rompecabezas, sino que elaboró la prueba desde el inicio hasta el final.
