2 ms·

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way

by kmoser 29d ago

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?

ezwoodland 28d ago
You can only do so in another framework that might itself have bugs. Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean". The kernel does have bugs sometimes.
- DoctorOetker 28d ago
  I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.
michael0church 28d ago
[dead]
- DoctorOetker 28d ago
  would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
  - dwheeler 28d ago
    Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
- torginus 28d ago
  So is there a chance that some of these AI-discovered proofs are actually Lean exploits?
  - ToValueFunfetti 28d ago
    This has happened: https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
    - qbit42 28d ago
      I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.
jibal 28d ago
You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of? https://www.youtube.com/watch?v=RxV4PQcJ1fw https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")
arlort 28d ago
In addition to what others added below you might be interested in this postmortem https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/ https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...
Jblx2 28d ago
You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean. https://arxiv.org/html/2403.14064v3 https://arxiv.org/html/2403.14064v3 https://github.com/digama0/lean4lean/tree/master https://github.com/digama0/lean4lean/tree/master

by kmoser 29d ago

Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?

ezwoodland 28d ago

You can only do so in another framework that might itself have bugs. Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean". The kernel does have bugs sometimes.

DoctorOetker 28d ago
I consider Metamath a lot more lean than "Lean", calling something such and so doesn't make it so in comparison to its peers.

michael0church 28d ago

[dead]

DoctorOetker 28d ago
would you assess Metamath systems more robust in adversarial settings, because the verifier is so short?
- dwheeler 28d ago
  Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
torginus 28d ago
So is there a chance that some of these AI-discovered proofs are actually Lean exploits?
- ToValueFunfetti 28d ago
  This has happened: https://github.com/leanprover/lean4/issues/14576 https://github.com/leanprover/lean4/issues/14576
  - qbit42 28d ago
    I have never seen an AI or a human produce a false proof without explicitly using weird meta programming tricks that are very suspicious. No "good faith" Lean proofs have every been shown faulty, to the best of my knowledge. While the risk is non-zero, many of the AI companies are also trying to find bugs in the Lean kernel, so it is becoming very well stress-tested.

jibal 28d ago

You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of? https://www.youtube.com/watch?v=RxV4PQcJ1fw https://www.youtube.com/watch?v=RxV4PQcJ1fw ("The Proof in the Code: How Lean Is Quietly Rewriting Trust in Math")

arlort 28d ago

In addition to what others added below you might be interested in this postmortem https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/ https://leodemoura.github.io/blog/2026-8-24-postmortem-for-t...

Jblx2 28d ago

You write your Lean4 type-checker in a way that is amenable to formal proof. And then verify properties of your type-checker. Like Lean4Lean. https://arxiv.org/html/2403.14064v3 https://arxiv.org/html/2403.14064v3 https://github.com/digama0/lean4lean/tree/master https://github.com/digama0/lean4lean/tree/master