El kernel de Lean presentó un fallo de solidez (bug #14576) que fue detectado y corregido durante la semana del 27 de julio. El origen fue la publicación, el 25 de julio, de un repositorio con una aparente refutación de la conjetura de Collatz generada con ayuda de IA y sin "sorry", obra de Ramana Kumar. Tres días después, Kiran Gopinathan redujo la prueba a una demostración de False y abrió el informe del bug. La corrección (#14577) se publicó una hora después y fue revisada por Joachim Breitner antes de su fusión.
El fallo afectaba a la eliminación de ocurrencias anidadas bajo un tipo inductivo T con parámetros Ds: cuando esos parámetros eran fantasma, desaparecían del tipo auxiliar generado, lo que permitía saltarse la comprobación de tipos y conseguir que el kernel aceptara una prueba de False. Solo se podía exploiting mediante metaprogramación, enviando la declaración inductiva directamente al kernel, ya que el frontend sí detecta el término mal tipado. Es un error de implementación, no una brecha en la metateoría de Lean.
El comprobador independiente nanoda, escrito en Rust por Chris Bailey, también falló: no verificaba el nombre de tipo en un nodo de proyección. Su bug fue reportado por Jeremy Chen y arreglado una semana antes. La prueba maliciosa aprovechaba que la expresión nunca inspeccionada por el kernel era precisamente la que el nanoda antiguo aceptaba. La verificación con un kernel independiente sigue siendo válida, pero exige ejecutar versiones actualizadas de ambos. Lean FRO ha incorporado pruebas de regresión, endurecido invariantes del kernel, integrado a nanoda en comparator.live y colabora con un modelo de IA de ciberseguridad de OpenAI para localizar más errores.