Lean 4.32.2 (2026-07-28)🔗

This point release fixes a soundness bug in the kernel.

The issue was discovered by Ramana Kumar and reported by Kiran Gopinathan.

A malicious meta program can trick the kernel into accepting a proof of False, or any other theorem. The kernel’s handling of nested inductive types with phantom type parameters was incomplete and bypassed the type checker.

The bug can be exploited even when using comparator.

The external checker nanoda does not suffer from the same bug. However, by the nature of this bug, it is possible to write proof terms that exploit it and at the same time exploit unrelated bugs in the external checker, as demonstrated by Kumar with a bug in nanoda that was (independently) reported and fixed very recently. We highly recommend users who have to account for malicious proofs and follow the recommended way to validate proofs to upgrade to the latest nanoda version as well.

The FRO takes these issues seriously and will invest in the checker ecosystem, towards more hardening, more testing and more independent implementations of kernels and checkers.

See issue #14576 for more details on the bug and PR #14577 for the fix.