Lean Bug Notes

• https://blog.trailofbits.com/2026/09/09/a-proof-of-fermats-last-theorem-that-fits-the-margin/
• https://github.com/leanprover/lean4/issues/10475
• https://github.com/leanprover/lean4/issues/10511
• https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/with/613492055

Kernel soundness bug #14576 and the follow-up bug hunt, from Leo de Moura’s postmortems (#14576, bug hunt):

• https://github.com/leanprover/lean4/issues/14576 (wrong-structure projections, axiom-free proof of False; fix: #14577, #14582)
• https://github.com/leanprover/lean4/pull/14613 (sorts not recognized as Prop up to universe normalization)
• https://github.com/leanprover/lean4/pull/14616 (declarations could name the kernel’s _nested auxiliary types)
• https://github.com/leanprover/lean4/pull/14806 (kernel is_def_eq caching was order-dependent)
• https://github.com/leanprover/lean4/pull/14807 (kernel is_prop check didn’t require a sort; also #14843 for inductive.h)
• https://github.com/leanprover/lean4/pull/14838 (runtime: refcount overflow corrupted objects)
• https://github.com/leanprover/lean4/pull/14833 (runtime: Linux CI built against GMP 6.1.2, which has an exploitable bug)

Found along the way, not soundness:

• https://github.com/leanprover/lean4/pull/14607 (missing check_no_metavar_no_fvar in inductive.cpp)
• https://github.com/leanprover/lean4/pull/14608 (universe params unchecked in mutual definitions)
• https://github.com/leanprover/lean4/pull/14609 (exported stubs of partial defs not marked unsafe)
• https://github.com/leanprover/lean4/pull/14615 (kernel rejected a valid inductive predicate)
• https://github.com/leanprover/lean4/pull/14849 (kernel didn’t bound computed Nat numeral size)

Via A critical look at Lean4 (Milo Moses, LessWrong).

LLVM and Coq both have collections of bugs. In Coq’s case, if memory serves, they are test .v files containing a reported bug.

It might be cool if there existed similar for Lean.