El verano en que la IA encontró errores de consistencia en Lean
What mathematicians should know about the Lean Theorem Prover: reliability & AI
Thomas Hales explica en un post invitado del blog de Terence Tao que la autoformalización con IA ya es una realidad: proyectos como la formalización del teorema de Fermat en 11 días o el de Navier-Stokes demuestran su potencial. Sin embargo, en 2026 aparecieron varios errores de consistencia en el kernel de Lean, el sistema de pruebas más usado por matemáticos. Hales sostiene que estos fallos, detectados por IA, son una señal positiva para la fiabilidad de las matemáticas.
El 'verano de los errores de consistencia de Lean' podría sonar a desastre, pero una investigación más detallada muestra que la detección de estos errores es un desarrollo positivo.
- chr15m
¿Volveremos a ver algún día un bug de solidez en el kernel de Lean?
Para un desarrollador de software, la pregunta parece una locura. Hubo bugs en el pasado, por supuesto que habrá más.
Cuando veamos esos bugs, ¿qué significará para las pruebas de Lean hechas por IA? ¿Podemos confiar en ellas?
Todo esto se reduce a la confianza.
Podemos confiar mucho en las verificaciones humanas gracias a la comunidad, la reputación y la prueba de trabajo humana. Los humanos a veces mienten sobre resultados matemáticos, pero es raro precisamente por esto. Cometen errores y esos errores son descubiertos por comunidades que a su vez son en gran medida confiables por esta misma razón.
A los LLM no les importa la reputación. Alucinan y fabrican a menudo. En los harnesses literalmente intentan hacer trampa y doblar las reglas, lo cual es un desastre para el conocimiento que está codificado en reglas. Así que tenemos que depender de los verificadores de pruebas.
El problema es: ¿qué tan confiables son los verificadores de pruebas? ¿Tienen bugs? ¿Y la teoría subyacente está libre de paradojas, indecidibles y "bugs" matemáticos que puedan explotarse? Imaginemos a un matemático humano empeñado en engañar a otros matemáticos: ¿confiaríamos en sus avances, incluso con un verificador?
Debido a estas propiedades, la última red de seguridad tienen que ser los humanos, y estar arraigada en la comunidad y en el sistema de confianza humana basado en prueba de trabajo. Por el momento, la gente está confiando demasiado en las herramientas.
Predicción: se encontrarán bugs por parte de humanos usando herramientas de IA que pongan en duda la prueba de Navier-Stokes.
- rramadass
El artículo ya menciona el paper Sets in Types, Types in Sets de Benjamin Werner, que mapea entre teorías de conjuntos y de tipos.
Otro paper relacionado y más accesible sobre la evolución de la teoría de tipos y su relación con las teorías de conjuntos y de categorías es Types, Sets and Categories de John Bell.
Por último, véase también Typed Lambda Calculus / Calculus of Constructions de Helmut Brandl para una excelente visión general, concisa pero con extensión de libro, del CoC/CIC.
En mi opinión, lo anterior es lectura obligatoria para entender los demostradores de teoremas y los asistentes de pruebas. En particular, la obra de Brandl es de lectura imprescindible.
- JonChesterfield
> La autoformalización se ha convertido en una realidad práctica en 2026
Eh, _quizás_. He estado traduciendo papers a Lean durante la última semana y la correlación entre el resultado formalizado y los papers es extremadamente pobre. El ciclo parece ser "intenta con el paper, es un poco difícil, demuestra algo distinto, proclama el éxito". Sigue siendo más rápido que hacerlo todo a mano, pero paper entra -> Lean sale de ninguna manera garantiza una correspondencia entre ambos.