Lean: 7 matemáticos advierten sobre formalizar todo con IA

Siete matemáticos —entre ellos Kevin Buzzard, una de las figuras centrales de Lean, el lenguaje de programación que verifica pruebas matemáticas— firmaron un texto colectivo que respalda formalizar toda la matemática con IA, pero con una advertencia dura: hacerlo rápido y sin curación humana puede ser un desperdicio de recursos y, peor, un daño duradero.

El debate parece académico y no lo es. Es el mismo problema que enfrenta cualquier equipo que hoy deja que un modelo genere código, documentación o análisis a escala.

Qué pasó antes de esta advertencia

El detonante fue la última publicación masiva de OpenAI. Según TechCrunch, la empresa liberó cientos de supuestas soluciones a problemas abiertos —719 manuscritos— después de haber consultado a un grupo asesor de matemáticos de élite: el Advisory Group on Mathematics and Artificial Intelligence (AGMAI), alojado en el Institute for Advanced Study.

El detalle incómodo está en las condiciones. La primera recomendación del AGMAI, publicada a fines de septiembre, fue dejar de testear problemas matemáticos avanzados en modelos propietarios. OpenAI lo hizo igual. Y de los 719 manuscritos, solo 10 incluyeron la cadena de razonamiento del modelo.

La Association for Human Mathematics respondió con una frase que resume el malestar del sector y que recogió Futurism: "Publicar más de 700 archivos de una vez no es una demostración de erudición, sino una demostración de poder". Terence Tao, medalla Fields, amplificó el comunicado y cuestionó que los problemas se resuelvan de forma autónoma por gente sin interés en el campo una vez que su objetivo inicial está resuelto.

Por qué una formalización que nadie usa no vale nada

El argumento central del texto es económico antes que matemático: un artefacto formal no vale nada si nadie lo usa. Los autores lo ilustran con tres casos.

• Math, Inc. y el empaquetado de esferas. Cuando esa empresa intentó apropiarse de un proyecto para formalizar los resultados de empaquetado de esferas en dimensiones altas de Maryna Viazovska, demostró lo que la tecnología podía hacer, pero no aportó nada a la matemática. El equipo original descubrió que limpiar el código generado por IA costaba más que reescribirlo desde cero.

• Fermat y las 13 millones de líneas. Anthropic anunció que Claude había verificado formalmente el Último Teorema de Fermat con 13 millones de líneas de código escritas en 11 días. Kevin Buzzard lo celebró y, al mismo tiempo, aclaró que no pensaba abandonar su propia formalización de una prueba más moderna: el código generado probablemente tenga poco valor sostenido.

• Navier-Stokes y la procedencia. Cuando OpenAI anunció soluciones a las ecuaciones de Navier-Stokes que explotan en tiempo finito, acompañó la prueba en lenguaje natural con una formalización en Lean. Ahí la señal de corrección sí importó. Pero, según Scientific American, el resultado —una solución de 166 páginas producida por unos 10.000 agentes que consumieron cerca de 88 horas de cómputo y 130.000 millones de tokens— desató el enojo de la comunidad por cómo se obtuvo, por la atribución de las ideas y por el desprecio a la comprensión humana.

El problema de fondo lo documentó un paper de matemáticos de la Universidad de Cambridge y King's College London, también reportado por TechCrunch: al menos dos discrepancias entre la prueba en lenguaje natural y el código Lean de la solución derivada de Navier-Stokes. No refutan el resultado, pero sí algo más importante para cualquier equipo: que un modelo formalice su propia salida no es garantía suficiente.

Los proyectos que ya construyen la biblioteca (y qué hacen distinto)

Los autores no piden parar. Piden mirar lo que ya funciona.

• Mathlib. La biblioteca comunitaria de código abierto que sostiene el ecosistema, curada por 65 revisores y con 950 contribuyentes hasta la fecha. Recibió el premio Jean-Pierre Demailly 2026 de Ciencia Abierta en Matemáticas. Crece más lento que las bibliotecas generadas por IA y, por eso mismo, es donde se aprenden las mejores prácticas.

• Tau Ceti. Incubada por la Lean FRO y la Mathlib Initiative. Todas las contribuciones las escriben IAs y luego las revisan otras IAs de forma adversarial con rúbricas estándar, siguiendo hojas de ruta curadas por matemáticos. Ya supera ligeramente a Mathlib: 3 millones de líneas de código. Entre sus resultados recientes están Riemann-Roch, la dualidad de Schur-Weyl y la densidad de Chebotarev.

• Formal Frontier. Un pipeline que convierte textos fuente en bibliotecas formales interconectadas usando un enjambre de agentes. Ya liberó 41 bibliotecas —unas 200.000 líneas— y está diseñado para ingerir miles de libros de texto.

• Palomar. Un registro que exige dos cosas a cada proyecto indexado: un archivo formalization.yaml con la descripción autoevaluada de qué se formalizó y cómo (solo humanos, con IA o de forma autónoma), y una configuración de Comparator para auditar qué prueba realmente el enunciado.

También mencionan Formal Conjectures, que recolecta enunciados formales de problemas abiertos, y el Annals Challenge de Buzzard, que busca enunciar —no probar— todos los teoremas de números recientes de Annals of Mathematics. El cuello de botella ahí son las definiciones faltantes, y el proyecto incentiva justamente formalizarlas bien.

Los principios que proponen

Del documento de valores de la comunidad de Mathlib, los autores derivan una lista que aplica a cualquier biblioteca formal:

• Deferir a las bibliotecas curadas por humanos, seguir sus reglas de diseño y refactorizar para adoptar sus decisiones.
• Preferir exhaustividad y amplitud antes que profundidad.
• Evitar duplicación: generalizar teoremas para maximizar la reutilización.
• Revisar los aportes públicamente, con estándares acordados.
• Publicar libremente: código abierto, interoperable y explorable.
• Mantenerse actualizado con cada release de Lean y Mathlib.
• Documentar y organizar, y enlazar con la literatura existente.
• Fijar estándares y cumplirlos: producir código de baja calidad y esperar "limpiarlo después" es contraproducente.

Qué significa esto para tu startup

Traducido a un equipo que usa IA para producir, el texto funciona como un manual de gestión de deuda técnica. La tesis: el costo de generar artefactos con IA cayó a casi cero, y eso convierte la curación en el cuello de botella —y en la ventaja competitiva.

Los tres modos de falla que describen son los mismos que aparecen en cualquier pipeline de código, documentación o contenido generado por modelos. Volumen sin uso. Procedencia opaca. Y revisión hecha por el mismo modelo que generó.

• Define un "terminado" que no sea "compila". En matemática, la corrección no basta: el valor está en que otro pueda construir encima. En tu equipo, un endpoint que responde no es un endpoint terminado. El criterio debería ser si otra persona puede extenderlo sin preguntarte nada.

• Exige metadatos de procedencia. El archivo formalization.yaml de Palomar es una idea exportable: por cada artefacto generado, deja registrado qué se generó, cómo (humano, asistido o autónomo) y con qué material previo se relaciona. Cuando el equipo cambie o el modelo se actualice, ese registro es lo único que te permite auditar.

• Separa generación de revisión. Tau Ceti no deja que el mismo agente valide su trabajo: otro agente lo revisa de forma adversarial contra una rúbrica. Es la versión barata de tener un revisor humano en cada pull request.

• Contribuye upstream en lugar de bifurcar. Los autores insisten en evitar la duplicación y en adoptar las decisiones de diseño de la biblioteca canónica. Cada fork propio es un costo de mantenimiento que se paga durante años.

Hay un punto extra para quien compra herramientas de IA: la pelea por los modelos propietarios es un adelanto del debate de procurement empresarial. El AGMAI pidió dejar de testear problemas avanzados en modelos cerrados porque la comunidad científica no puede acceder a ellos. Si tu producto depende de un modelo que no puedes auditar, tu capacidad de verificar tus propios resultados tiene el mismo techo.

Conclusión

Los autores son optimistas y lo dicen: en un plazo de tres años, y posiblemente antes, la mayor parte de la matemática podría estar formalizada de forma que los matemáticos puedan explorarla y construir sobre ella. La Lean FRO se comprometió a sostener proyectos de esa escala.

Pero la frase que ordena todo el texto es una condición: el retorno justificaría una inversión enorme "si y solo si lo hacemos bien". Ese "si y solo si" es la parte que casi nadie quiere leer, y es la que decide si la IA multiplica el conocimiento o solo produce archivos que nadie abre.

Fuentes

• How to Formalize All of Mathematics (fuente original)
• OpenAI's math solutions aren't meeting the field's standards yet
• OpenAI's blockbuster math proof isn't what you think it is
• Mathematicians React With Fury as OpenAI Releases Hundreds of New AI-Generated Proofs