Investigadores del Departamento de Matemáticas del MIT, David Roe y Andrew Sutherland, han sido seleccionados como los primeros beneficiarios de las becas AI for Math, una iniciativa de Renaissance Philanthropy y XTX Markets. Este reconocimiento también se extiende a otros cuatro alumni del MIT: Anshula Gandhi, Viktor Kun?ak, Gireeja Ranade y Damiano Testa, quienes han sido premiados por proyectos distintos.
Las 29 iniciativas ganadoras están diseñadas para respaldar a matemáticos e investigadores en universidades y organizaciones que buscan desarrollar sistemas de inteligencia artificial destinados a impulsar el descubrimiento y la investigación matemática en diversas tareas clave.
Avances en la Prueba Automatizada de Teoremas
Roe y Sutherland, junto con Chris Birkbeck de la Universidad de East Anglia, utilizarán su financiación para potenciar la prueba automatizada de teoremas. Su enfoque se centrará en crear conexiones entre la Base de Datos LMFDB y la biblioteca matemática Lean4 (mathlib).
Sutherland destaca que “los probadores automáticos de teoremas son técnicamente complejos, pero su desarrollo carece de recursos”. La llegada de tecnologías como los modelos de lenguaje grande (LLMs) está reduciendo rápidamente las barreras para acceder a estas herramientas formales, facilitando su uso por parte de matemáticos en activo.
Conectando Bases de Datos Matemáticas
Mathlib, una extensa biblioteca matemática impulsada por la comunidad para el probador de teoremas Lean, contiene alrededor de 100,000 resultados matemáticos. Por su parte, la LMFDB es un recurso colaborativo que abarca más de mil millones de declaraciones concretas relacionadas con la teoría moderna de números. Tanto Roe como Sutherland son editores responsables de esta base de datos.
El proyecto financiado tiene como objetivo integrar ambos sistemas, permitiendo que los resultados disponibles en LMFDB se presenten dentro de mathlib como afirmaciones aún no formalmente demostradas. Además, se proporcionarán definiciones formales precisas para los datos numéricos almacenados en LMFDB. Esta conexión beneficiará tanto a matemáticos humanos como a agentes de inteligencia artificial, ofreciendo un marco para vincular otras bases matemáticas con sistemas formales de prueba teórica.
Desafíos en el Descubrimiento Matemático Automatizado
A pesar del progreso, existen obstáculos significativos para automatizar el descubrimiento y la prueba matemática. Estos incluyen la escasez de conocimiento matemático formalizado y el alto costo asociado a la formalización de resultados complejos. Para abordar estos desafíos, los investigadores planean utilizar los fondos recibidos para crear herramientas que faciliten el acceso a LMFDB desde mathlib.
Esta estrategia permitirá que los asistentes en pruebas identifiquen objetivos específicos para su formalización sin necesidad de formalizar previamente toda la base de datos LMFDB. Roe señala que “disponer de una amplia base de datos no formalizada dentro de mathlib proporcionará una técnica poderosa para el descubrimiento matemático”, ya que el conjunto inicial puede ser considerablemente mayor al número final necesario para probar un teorema específico.
Nuevas Perspectivas en Teoría Numérica
A medida que se avanza hacia nuevas fronteras del conocimiento matemático, demostrar nuevos teoremas frecuentemente implica cálculos no triviales. Un ejemplo emblemático es la prueba del Último Teorema de Fermat realizada por Andrew Wiles, que utiliza lo que se conoce como “el truco 3-5” en un punto crucial del argumento.
Sutherland explica que este truco depende del hecho conocido sobre la curva modular X_0(15), lo cual es fácil verificar con herramientas computacionales modernas pero difícilmente puede ser demostrado manualmente. Conectar probadores formales con sistemas algebraicos computacionales ofrece beneficios adicionales al aprovechar resultados precomputados ya existentes.
Pasos Futuros y Colaboración Abierta
"Los próximos pasos incluyen formar un equipo, interactuar con las comunidades LMFDB y mathlib, comenzar a formalizar definiciones fundamentales relacionadas con curvas elípticas y otros campos relevantes", afirma Roe. Además invita a estudiantes del MIT interesados a participar activamente en esta emocionante iniciativa.
Si (
No(
