OpenAI retiró tres manuscritos de demostraciones matemáticas producidos por un modelo interno de inteligencia artificial el 7 de octubre de 2026. Un error de signo invalidó un argumento de un trabajo y una construcción utilizada por otros dos. Esto no demuestra que fallara el verificador Lean. Lean puede comprobar que una deducción formal se sigue de determinadas hipótesis, pero esa comprobación por sí sola no garantiza que el enunciado formal coincida con el problema matemático que se pretendía resolver ni que el resultado sea un descubrimiento nuevo.
De la publicación a las correcciones: la cronología documentada
El 6 de octubre, OpenAI publicó 722 manuscritos agrupados en 372 familias de resultados en el repositorio público openai/math. La empresa atribuyó los materiales a un modelo interno todavía no disponible y describió los trabajos como resultados de investigación en distintas fases de verificación. En este contexto, una prepublicación es un documento difundido antes de la revisión tradicional por pares, no una certificación definitiva.
En su historial del 7 de octubre, la compañía retiró tres trabajos, revisó otros 14 manuscritos con reparaciones de pruebas y modificaciones de hipótesis, enunciados o referencias, y actualizó 13 más para que citaran las versiones corregidas. La misma entrada registró seis formalizaciones adicionales e indicó que 300 resultados principales de 719 manuscritos estaban formalizados en Lean, aproximadamente el 42 %. Era el cálculo divulgado por OpenAI en aquella fecha, no una auditoría independiente de todos los archivos.
El catálogo siguió evolucionando. El 26 de octubre, OpenAI añadió dos manuscritos con sus respectivas formalizaciones; el README consultado el 30 de octubre indicaba 721 manuscritos en 373 familias. El 29 de octubre, el historial anotó una corrección de espacios de nombres entre el desafío y la solución de Comparator para otro resultado, sobre variedades abelianas CM. Ese cambio no debe confundirse con las retiradas del 7 de octubre ni con el trabajo retirado sobre productos de superficies K3.
¿Qué tres manuscritos fueron retirados?
El historial oficial identifica los trabajos con estos títulos originales:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
El primer manuscrito contenía un error de signo que invalidaba un argumento de cancelación relacionado con trazas de estabilización. Los otros dos dependían de la construcción afectada. Por eso se retiraron los tres y se publicaron avisos sobre la laguna, con enlaces a las versiones archivadas. Se trata de un defecto en el razonamiento presentado, no de una demostración de que las propias conjeturas sean falsas.
¿Qué verifica realmente Lean?
Lean es un lenguaje de programación y un asistente interactivo de demostración formal. En lugar de aceptar una explicación en lenguaje natural porque parece convincente, su núcleo verificador comprueba si un objeto de prueba demuestra una proposición formulada mediante definiciones y reglas lógicas precisas. Su documentación distingue la búsqueda de una prueba de su comprobación: un sistema de IA puede proponer el razonamiento, mientras que el verificador evalúa su representación formal.
Esa garantía está condicionada al enunciado formal, las definiciones, los axiomas y las dependencias empleados. Un teorema puede estar correctamente demostrado en Lean y, aun así, abordar una versión más restringida, distinta o mal traducida de una afirmación matemática informal. Por ejemplo, demostrar una propiedad para una clase especial de objetos no equivale a demostrarla para todos los objetos, aunque la prueba formal sea impecable.
El manual de Lean advierte que una señal visual de aprobación no basta para todas las auditorías: las dependencias pueden contener sorry, un marcador de pasos pendientes que se convierte en un axioma. El comando #print axioms permite examinar los axiomas y supuestos empleados, incluidas las dependencias indirectas. Para una comprobación más exigente, lean4checker y comparator aportan controles adicionales; Comparator contrasta el teorema demostrado con un enunciado de desafío preparado de forma confiable. Incluso ese procedimiento depende de que el desafío y sus definiciones sean correctos.
Tres preguntas que no deben confundirse
| Nivel | Qué se examina | Límite decisivo |
|---|---|---|
| Validez lógica | ¿La demostración formal se sigue de las definiciones, axiomas y premisas declaradas? | La comprobación técnica no corrige automáticamente un enunciado mal planteado. |
| Fidelidad del enunciado | ¿La proposición codificada expresa la conjetura original sin debilitarla? | Exige un análisis matemático del significado de las definiciones y las hipótesis. |
| Aportación científica | ¿El resultado es nuevo, relevante, comprensible, debidamente atribuido y sometido a escrutinio académico? | Requiere revisar la literatura, recibir críticas independientes y debatir científicamente; compilar código no basta. |
La opinión de los matemáticos y el origen de las reservas
En una información del 8 de octubre, Retraction Watch publicó que, según un portavoz de OpenAI, el error se había detectado durante una auditoría de la propia empresa. Alex Townsend, de la Universidad Cornell, sostuvo que los trabajos ya formalizados deberían haberse difundido por separado. Andrew Sutherland, del MIT, consideró adecuada la rápida retirada, pero señaló que recuperar la confianza exigiría más trabajo. Son valoraciones atribuidas a esos investigadores, no un dictamen universal de la comunidad matemática.
En recomendaciones publicadas el 29 de septiembre de 2026, el grupo asesor independiente AGMAI pidió transparencia sobre el modelo, las instrucciones, los problemas intentados, el coste computacional, las formalizaciones y la identificación clara de los trabajos todavía no verificados. También destacó la comprensión humana, la revisión por pares cuando proceda y la conservación del historial de correcciones. Sus recomendaciones permiten publicar trabajos sin formalización completa bajo condiciones de transparencia, pero esa difusión no equivale a una validación científica.
El 26 de octubre, la propia OpenAI pasó a describir los manuscritos generados por IA como datos brutos de investigación y anunció diferentes fórmulas de colaboración con especialistas externos para explicar nuevos resultados. Este cambio de procedimiento no valida de forma retroactiva los tres trabajos retirados.
Qué permite concluir el episodio
La conclusión documentada es concreta: tres argumentos publicados no se sostenían tal como fueron divulgados y OpenAI corrigió o actualizó otros trabajos. Esto no permite afirmar que todo el catálogo sea inválido, que Lean aprobara aquellas tres demostraciones ni que su núcleo verificador tuviera un defecto. Los documentos consultados no incluyen una ejecución independiente de las formalizaciones por parte de DTech ni una comprobación exhaustiva de todos los manuscritos.
Para evaluar una nueva prueba matemática producida por IA, hay que saber qué enunciado se formalizó exactamente, si se auditaron los axiomas y las dependencias, qué parte del razonamiento se comprobó, quién evaluó la correspondencia con la conjetura original y qué revisión científica se llevó a cabo. La comprobación lógica responde a una pregunta esencial, pero no sustituye a las demás.
Fuentes y referencias
- OpenAI, anuncio del 6 de octubre
- OpenAI, repositorio y estado del catálogo
- OpenAI, historial de retiradas y correcciones
- Lean, manual de validación de pruebas formales
- Lean, introducción a la demostración de teoremas
- Retraction Watch, información independiente del 8 de octubre
- AGMAI, recomendaciones del 29 de septiembre
- OpenAI, modelo de colaboración anunciado el 26 de octubre
