Las IA generativas encuentran errores de código (bugs) donde nadie los espera. Incluso en el núcleo de Lean (el verificador automático de demostraciones matemáticas más famoso). El 25 de julio de 2026, Ramana Kumar publicó en GitHub una formalización en Lean de la refutación de la famosa conjetura de Collatz. Producida por una IA, esta vez nadie se creyó que existiera un entero positivo cuya órbita de Collatz nunca alcanza 1. La refutación era existencial y no mostraba dicho entero, luego tenía que ser incorrecta. El 28 de julio, Kiran Gopinathan descubrió que la supuesta demostración explotaba un bug del kernel de Lean. El bug #14576 permitía demostrar que Falso es Verdadero (Gopinathan lo demostró con un sencillo ejemplo). El equipo que mantiene el kernel de Lean lo ha reforzado para evitar bugs similares. Pero en Informática nunca digas nunca jamás. Nadie sabe si aparecerá algún otro bug similar. Por ello, no basta con que Lean (u otro software) valide una demostración matemática, siempre es necesario la validación independiente mediante varios software diferentes.

Kumar es un prestigioso experto en métodos formales y en lenguajes de verificación automática de demostraciones. Su trabajo más famoso es el lenguaje funcional CakeML, una implementación del lenguaje ML que está verificada de forma automática. Kumar conoce muy bien el kernel de Lean y usó una IA para buscar sus debilidades. Gracias a dicha IA encontró una «sorry-free ‘disproof’» (algo que acepta el demostrador automático pero que no debería haber sido aceptado). Aprovecharla para probar que Falso es Verdadero era algo trivial con poco impacto mediático, así que prefirió publicar algo más sensacionalista, una refutación de la conjetura de Collatz. Nos cuenta los detalles Leonardo de Moura, «Postmortem for Kernel Soundness Bug #14576,» Blog, 01 Aug 2026. Resumiendo, un metaprograma en Lean llamado deriveLimit lograba manipular la representación interna de las expresiones usando cosas como mkApp, mkProj y mkLambda, hasta introducir una declaración mediante addDecl <| .thmDecl {…}. Gracias a este addDecl se podía declarar Falso como Verdadero y a partir de ahí demostrar cualquier cosa. Por fortuna, el error del kernel ha sido resuelto de forma rápida, eficaz y pública.

Los metaprogramas son claves para simplificar la escritura de demostraciones pues permiten convertir theorem foo : … en expresiones internas explícitas. Estos metaprogramas están fuera de la base de confianza lógica y, a priori, pueden contener bugs sin que afecten a la ejecución del kernel. Se consideran seguros porque si generan una expresión mal tipada, el kernel debe rechazarla. La metaprogramación no se puede prohibir en Lean. Pero la seguridad lógica del kernel debe garantizar que todo término mal formado debe ser detectado y la validación en curso debe finalizar. El bug #14576 lograba esquivar la finalización, permitiendo incorporar contenido absurdo de consecuencias nefastas. La resolución del bug impide aprovechar esta vía en el futuro.

Gopinathan logró mostrar la esencia del fallo aprovechado por la falsa refutación de Collatz. Se define el constructor inductive T : Bool → Prop | mk : T true, que construye T como verdadero, sin que exista un constructor de T como falso. El bug #14576 permitía que Lean aceptase un término bad : T false, aunque tal término no debería poder existir. Gracias a ello, basta el teorema theorem boom : False := nomatch (bad : T false), para que Lean 4 (con el fallo en el kernel) resonda que tanto bad como boom no dependen de ningún axioma. Así el kernel aceptaba dicha demostración de que T es verdadero (por el axioma) y falso (por bad) de forma simultánea. Y, por supuesto, después de aceptar Falso como Verdadero se puede «demostrar cualquier cosa». En Lean, tras boom : False puedes escribir theorem prove_anything (P : Prop) : P := False.elim boom, y sustituir P por 1 = 2 (o RiemannHypothesis, o ¬ RiemannHypothesis, o Collatz.Conjecture, o ¬ Collatz.Conjecture, etc.).

Quizás te lo preguntes, ¿bug #14576? ¿Tantos bugs hay acumulados? El núcleo de Lean está escrito en C++ y tiene unas 6000 líneas, mientras que Mathlib supera 1.5 millones de líneas de código escritas en el propio Lean (este código está verificado). El 22 de julio de 2026, Patrick Hulin, ayudado por GPT-5.6 Sol, descubrió otro bug en el kernel de Lean, bug #14484. Ese bug también permitía demostrar Falso, pero mediante un mecanismo distinto. Fue corregido por Joachim Breitner mediante PR #14498 el mismo 22 de julio.

Lo más sorprendente del bug #14576 es que fue un «doble bug», porque la incorrecta refutación de Collatz no solo se verificó en Lean, Kumar también la verificó en Nanoda, una implementación independiente de Lean desarrollada en el lenguaje Rust. A priori, un doble bug en Lean y Nanoda es muy improbable. De hecho, el bug de Nanoda era diferente y fue reportado por Jeremy Chen; se logró corregir antes que el bug de Lean. No conocemos los entresijos del trabajo de Kumar con su IA para descubrir estos bugs. Pero me atravo a conjeturar que Kumar partió del bug en Nanoda y con ayuda de una IA buscó un bug similar en Lean 4; tras encontrarlo decidió aproveharlo para lograr un minuto de gloria en redes sociales refutando la conjetura de Collatz en Lean y Nanoda. Cuidado, todo esto es una conjetura mía (hasta donde me consta Kumar no ha contado nada sobre lo que hizo).

Por cierto, el informe sobre el bug #14576 se abrió el 28 de julio. Leonardo de Moura, creador y arquitecto jefe de Lean, inició la reparación con el PR #14577, dándola por finalizada una hora más tarde. La resolución (fix) fue revisada y mejorada por Joachim Breitner. También reforzó la solución Arthur Adjedj. Así que fue un trabajo de todo el equipo dedicado a mantener el kernel de Lean, que resultó en la publicación de la versión 4.32.2, publicada el 28 de julio de 2026. Y, por último, la figura sobre la conjetura de Collatz es de Vitaliy Kaurov, «A beautiful picture related to Collatz conjecture,» WOLFRAM Research, 2015.