00:54:13 <DataHoarder> Related to formally proving incoming new methods, a soundness bug was found on Lean https://github.com/leanprover/lean4/issues/14576
00:55:36 <DataHoarder> some writing around it https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/
11:59:15 <br-m> <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 https://github.com/leanprover/lean4/issues/14576
12:00:02 <DataHoarder> Lean -> Lean kernel (implementation) correct