CVE-2026-72844

Resumo

O kernel do Lean 4 não verifica se a estrutura nomeada em uma expressão de projeção corresponde ao tipo do valor que está sendo projetado, e `environment::add_inductive` em `src/kernel/inductive.cpp` não fazia a verificação de tipo das aplicações indutivas aninhadas que são substituídas por tipos auxiliares, de modo que seus argumentos paramétricos escapavam da verificação. Um metaprograma executado no processo Lean pode registrar um indutivo aninhado mal tipado cujo construtor aplica uma projeção `.proj C 0` a um valor do tipo não relacionado `W`, e o kernel admite a declaração pelo caminho comum de `addDecl` verificado no nível máximo de verificação do kernel, sem `sorry`, `unsafeCast`, `debug.skipKernelTC`, `addDeclWithoutChecking`, FFI ou um arquivo `.olean` modificado. O resultado é uma confusão de tipos que produz uma prova de `False` sem axiomas, a partir da qual qualquer proposição pode ser derivada. A prova de conceito publicada adicionalmente preenche duas expressões até que seus hashes e profundidades aproximadas colidam, o que anula o cache do kernel; essa é a técnica usada para alcançar a falha, não a sua causa. A exploração exige executar um metaprograma no processo, por exemplo, construindo um projeto ou importando uma dependência Lake maliciosa.

• lean-cve-pocPoC

  CVE-2026-72844 : Exemplo de prova de "0 = 1" usando uma vulnerabilidade no kernel do Lean 4.