- Sources: lean4 issue 14576, lean4 PR 14577, HN 49082495
- Summary: Issue 14576 was opened 2026-07-28 at 03:28 UTC by kiranandcode against nightly 4.34.0-nightly-2026-07-27. The repro adds declarations through the ordinary checked
addDecl path and then proves False, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified olean file, and it still passes under lean --trust=0. Lean prints that both the intermediate theorem and the final term depend on no axioms, so print axioms does not flag the result. Leonardo de Moura opened the fix as PR 14577 at 05:08 UTC and it merged at 13:39 UTC the same day, closing the issue. The PR gives the cause: when eliminating a nested occurrence, the parametric arguments were dropped from the generated auxiliary types and so escaped type checking, and they are now checked once the inductive types being declared are available. Joachim Breitner added a regression case to the leanprover/lean-kernel-arena repository at 09:47 UTC. Exploitation requires an adversarial metaprogram rather than ordinary Lean source. The reporter found it while reviewing a claimed sub-300-line proof of the Collatz Conjecture by xrchz. The fix is in the Lean tree and is not in a tagged release as of publication. - Why it matters: A soundness hole in a proof assistant's trusted kernel is the exact failure the kernel exists to rule out, and a team on a tagged toolchain should not assume it carries the fix yet.
- Follow-up: Watch for the first tagged Lean release carrying PR 14577.
send feedback on this story