Fuente: La 100.
OpenAI publicó en GitHub un repositorio con 722 demostraciones matemáticas producidas mediante inteligencia artificial y verificadas con Lean, un asistente informático especializado en comprobar la consistencia lógica de las pruebas. Los resultados fueron organizados en 372 familias de teoremas y abarcan distintas áreas de investigación matemática avanzada.
Cómo se hicieron las demostraciones matemáticas generadas con IA
Las demostraciones se enfocan en campos complejos como la teoría analítica de números, la álgebra conmutativa, la topología diferencial y la geometría algebraica. Cada trabajo incluye el código necesario para que Lean pueda verificar la prueba, una explicación formal en lenguaje matemático y referencias a resultados previos utilizados durante el desarrollo.
La escala del proyecto resulta llamativa si se la compara con Mathlib, la principal biblioteca pública de matemáticas formalizadas de Lean 4, que reúne cerca de 200.000 teoremas acumulados a lo largo de años de trabajo colaborativo. Aunque la cantidad de resultados generados por OpenAI es significativa, los especialistas remarcan que el volumen no determina por sí mismo la importancia científica de los hallazgos.
Según explicó la empresa, cada demostración requirió aproximadamente tres horas de procesamiento utilizando ChatGPT Pro en modo de razonamiento extendido. En conjunto, el proyecto demandó más de 2.100 horas de cómputo, una cifra que refleja la complejidad del proceso.
Aunque OpenAI no informó cuánto dinero destinó al proyecto, estimaciones difundidas por analistas del sector indican que la iniciativa habría requerido decenas de miles de dólares en recursos de inferencia y potencia computacional.
El futuro de la matemática asistida por IA
Uno de los puntos más debatidos es la diferencia entre una prueba formalmente válida y un resultado con verdadero impacto científico. El mismo sistema fue utilizado en julio de 2026 para presentar una propuesta relacionada con las ecuaciones de Navier-Stokes, uno de los históricos Problemas del Milenio, aunque esa investigación todavía continúa bajo revisión de expertos.
Investigadores como Tristan Buckmaster, de la Universidad de Princeton, advirtieron que la verificación de Lean garantiza la coherencia lógica de una demostración, pero no determina automáticamente si el resultado responde de manera efectiva a una pregunta matemática abierta o relevante.
La publicación representa un nuevo paso en la aplicación de la inteligencia artificial a la investigación científica. Estas herramientas ya demostraron capacidad para acelerar la construcción, revisión y validación de pruebas complejas, reduciendo tiempos de trabajo que tradicionalmente demandaban meses o incluso años.
