DigiNews

Summary

This postmortem describes a Lean kernel soundness bug (#14576) caused by how nested inductive types interact with phantom parameters, which could allow a false proof to pass. A fix was pushed within an hour, with discussion on nanoda, metaprogramming, and independent kernel checks. It emphasizes that this is a kernel implementation bug, not a flaw in Lean's meta-theory, and outlines follow-up tests and improvements.