www.lesswrong.com/posts/zHhGa3iQBQcdSifFL/a-critical-look-at-lean4-1

The linked Lean posts contradict the specific count here.

• In Leo de Moura’s August 1, 2026 postmortem for bug #14576, he writes that Daniel Selsam at OpenAI assisted the Lean FRO and found other programming mistakes in the Lean kernel, then lists exactly six PRs: #14607, #14608, #14609, #14613, #14615, #14616.
• In the later August 24, 2026 “kernel soundness bug hunt” post, Leo does not summarize the result as “seven more bugs in the kernel.” Instead, he separately lists:
  • 4 kernel soundness bug-fix items in official kernel code (#14613, #14616, #14806, #14807/#14843),
  • 2 runtime exploits (#14838, #14833), and
  • 5 other bug/hardening PRs (#14607, #14608, #14609, #14615, #14849).

So the claim is inaccurate on its face: the authoritative follow-up posts do not give a total of seven additional kernel bugs, and the later linked post explicitly includes some issues that were runtime problems rather than kernel bugs. The same sources also attribute the discoveries to work involving Daniel Selsam / OpenAI internal models assisting the Lean FRO, not simply “the Lean FRO found seven more bugs.”

This statement is too strong to be true.

There are public specifications and formalizations of Lean’s theory:

• The lean4lean project publicly exposes an abstract theory layer: its README says Lean4Lean.Theory contains “the Lean metatheory and properties,” and Lean4Lean.Verify is “the proof that the Lean4Lean implementation satisfies the Lean4Lean.Theory abstract specification.” That is exactly a public spec to track against, even if the work is incomplete.
• Leo de Moura’s August 24, 2026 postmortem says lean-inductive-models addresses concerns about whether Lean’s inductive-type theory is understood, and states: “The same derivation demonstrates that the constructions Lean uses are well understood. The soundness bugs in this area were implementation mistakes, not gaps in the theory.”

That does not mean every consistency or metatheory question is fully settled. But it does directly contradict the absolute claim that “nobody knows how Lean4’s type theory is supposed to behave” or that there is “no spec to track.” Public specs, models, and implementation-vs-theory verification efforts already exist.