Related to formally proving incoming new methods, a soundness bug was found on Lean leanprover/lean4 #14576

some writing around it leodemoura.github.io/blog/2026-8-1-…rtem-for-kernel-soundness-bug-14576

<basses:matrix.org> > This is an implementation bug, not a hole in Lean's meta-theory. > <DataHoarder> Related to formally proving incoming new methods, a soundness bug was found on Lean leanprover/lean4 #14576

Lean -> Lean kernel (implementation) correct