OpenAI publica 722 demostraciones matemáticas generadas por IA y verificadas con Lean
OpenAI ha publicado en GitHub un repositorio con 722 demostraciones matemáticas generadas por inteligencia artificial, agrupadas en 372 familias de teoremas. Todos los resultados han sido comprobados formalmente con Lean, un asistente de pruebas que verifica paso a paso si un argumento es lógicamente válido.
El corpus está disponible desde el 7 de octubre en github.com/openai/math y reúne problemas de investigación activa en distintas ramas de las matemáticas puras. La compañía sostiene que se trata de la mayor colección de demostraciones matemáticas generadas por IA publicada hasta la fecha.
Más de 700 resultados en una sola publicación
La dimensión del lanzamiento se entiende mejor al compararla con Mathlib, la gran biblioteca comunitaria de matemáticas formalizadas para Lean 4. Este proyecto acumula alrededor de 200.000 teoremas construidos durante años de trabajo colaborativo. OpenAI ha añadido ahora 722 demostraciones nuevas en una única entrega.
Los manuscritos no se limitan a ejercicios académicos conocidos. El repositorio incluye trabajos relacionados con la teoría de números analítica, el álgebra conmutativa, la topología diferencial y la geometría algebraica, áreas que habitualmente requieren una preparación matemática avanzada.
Cada resultado incorpora tres elementos principales: el archivo escrito en Lean que permite verificarlo, una explicación en lenguaje matemático natural y las referencias a los teoremas previos de los que depende. Esta estructura facilita que otros investigadores puedan revisar, reutilizar o ampliar el trabajo.
Qué aporta la verificación formal
Los modelos de lenguaje de gran tamaño, conocidos como LLM, pueden generar textos con apariencia matemática convincente, pero también introducir errores sutiles. Una demostración puede parecer correcta y contener un salto lógico, una hipótesis omitida o una conclusión que no se desprende de los pasos anteriores.
Lean funciona como un comprobador automático. El investigador o el sistema de IA debe expresar cada paso utilizando reglas y objetos matemáticos formalizados. Si la demostración contiene una inconsistencia, el verificador la rechaza. Si se acepta, significa que el argumento cumple las reglas lógicas y definiciones incluidas en el sistema.
Esta distinción es importante: la verificación formal confirma la consistencia lógica de una prueba, pero no determina por sí sola su relevancia científica. Un resultado puede ser impecable desde el punto de vista formal y, al mismo tiempo, resolver una versión secundaria de un problema o aportar una conclusión poco significativa para la comunidad.
Un proceso que exige miles de horas de cómputo
La generación del corpus no se ha producido de forma instantánea. Cada demostración habría requerido aproximadamente tres horas de ChatGPT Pro en un modo de razonamiento extendido. En conjunto, el proceso representa más de 2.100 horas de cómputo acumulado.
OpenAI no ha detallado el coste total de la infraestructura empleada. Sin embargo, el volumen de tiempo de inferencia —el proceso mediante el que un modelo genera una respuesta a partir de sus parámetros— apunta a una inversión de varias decenas de miles de dólares, según las tarifas actuales de sus servicios.
El dato ilustra una de las características de la actual carrera por los sistemas de razonamiento: obtener mejores resultados no depende únicamente de entrenar modelos más grandes. También requiere dedicar más tiempo de procesamiento a cada problema, explorar distintas estrategias y comprobar las respuestas antes de darlas por válidas.
El mismo sistema que abordó Navier-Stokes
El sistema utilizado para producir el repositorio es el mismo que OpenAI presentó en julio al anunciar una solución para un problema abierto relacionado con las ecuaciones de Navier-Stokes. Estas ecuaciones describen el comportamiento de fluidos como el agua o el aire y forman parte de los siete Problemas del Milenio del Clay Mathematics Institute, cada uno asociado a un premio de un millón de dólares.
La supuesta solución continúa en proceso de revisión por pares. En matemáticas de frontera, la comprobación independiente de un resultado puede prolongarse durante meses, especialmente cuando intervienen argumentos muy extensos o nuevas técnicas.
Además, algunos especialistas han cuestionado el alcance de aquella contribución. Tristan Buckmaster, investigador de la Universidad de Princeton especializado en ecuaciones diferenciales parciales, ha señalado que una prueba puede ser formalmente válida y no abordar necesariamente el núcleo de la pregunta que la comunidad considera abierta.
El equipo asesor de AGMAI, la coalición encargada de evaluar la solución de Navier-Stokes, ha planteado una advertencia similar. La formalización garantiza que no hay errores lógicos dentro del marco definido, pero no sustituye la valoración humana sobre la profundidad, la originalidad o la importancia del resultado.
IA como colaboradora, no como sustituta
El nuevo corpus refuerza la idea de que los agentes de inteligencia artificial pueden asumir tareas científicas cada vez más complejas. En este caso, no se limitan a explicar teoremas o sugerir pasos: generan demostraciones, las traducen a un lenguaje formal y las someten a un proceso automático de comprobación.
La principal aportación está en acelerar una parte del trabajo matemático que consume mucho tiempo: construir argumentos detallados, localizar resultados previos y detectar fallos formales. Aun así, el sistema no resuelve una cuestión esencial: decidir qué problemas merecen ser investigados y qué dirección puede conducir a un avance relevante.
También quedan abiertas cuestiones sobre la autoría y la reproducibilidad. La comunidad matemática tendrá que establecer cómo atribuir crédito a resultados creados con modelos propietarios, cómo citar sistemas que pueden cambiar con una actualización y qué nivel de supervisión humana debe exigirse.
Las 722 demostraciones representan, por tanto, un logro técnico significativo, sobre todo por su verificación con Lean. Pero el salto desde una prueba válida hasta una contribución matemática profunda sigue dependiendo de la evaluación, la intuición y el criterio de los investigadores.
