Lean 4 kernel soundness bug: forging proofs via nested inductive projections (0 = 1 demonstrated)

<p>Posted by Jonathan Brossard on Aug 01</p>Dear list,<br /> <br /> I hope this email finds you well.<br /> <br /> I&apos;d like to bring attention to a soundness vulnerability in the Lean 4<br /> theorem prover kernel that allows a malicious metaprogram to cause the<br /> kernel to accept invalid proofs, including proofs of false statements<br /> such as False and 0 = 1, with no axioms and full k