CVE-2026-72844

Resumen

El kernel de Lean 4 no verifica que la estructura nombrada en una expresión de proyección coincida con el tipo del valor sobre el que se proyecta, y environment::add_inductive en src/kernel/inductive.cpp no comprobaba los tipos de las aplicaciones inductivas anidadas que se sustituyen por tipos auxiliares, por lo que sus argumentos paramétricos escapaban a la comprobación. Un metaprograma que se ejecuta en el proceso de Lean puede registrar un inductivo anidado mal tipado cuyo constructor aplica una proyección .proj C 0 a un valor del tipo no relacionado W, y el kernel admite la declaración a través de la ruta ordinaria de addDecl comprobada con la comprobación máxima del kernel, sin sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI ni un archivo .olean modificado. El resultado es una confusión de tipos que produce una prueba de False sin axiomas, a partir de la cual se puede derivar cualquier proposición. La prueba de concepto publicada además rellena dos expresiones hasta que sus hashes y profundidades aproximadas colisionan, lo que anula la caché del kernel; esa es la técnica utilizada para alcanzar la falla, no su causa. La explotación requiere ejecutar un metaprograma dentro del proceso, por ejemplo compilando un proyecto o importando una dependencia maliciosa de Lake.

• lean-cve-pocPoC

  CVE-2026-72844 : Ejemplo de demostración de "0 = 1" utilizando una vulnerabilidad en el kernel de Lean 4.