Why Is It All in the Kernel?
A recent proof refuting the Collatz conjecture, checked by Lean and Nanoda, turned out to be wrong due to a kernel bug. This incident highlights the risks of relying on proof objects and complex kernel features. The author argues for a minimalist kernel with derived definitions, as in HOL Light or Isabelle, contrasting 'honest toil' with 'theft' in proof assistant design.
The method of 'postulating' what we want has many advantages; they are the same as the advantages of theft over honest toil.
- yjftsjthsd-h
Proof assistant kernel, not operating system kernel - in case, like me, you clicked in hoping to debate the merits of microkernels vs monolithic:) Although I suppose there is a significant analogy, since the argument here... if I understood right... is very close to the classic 'and now a small defect in a device driver just panicked the system or gave an attacker root', just in math terms.
- red_trumpet
Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
- f12a8h
We have to remember that OpenAI wanted us to believe that an adversarial AI hacked Huggingface because it was "too ambitious".
Then an AI found a proof of False, hidden in the "proof" of the Collatz conjecture.
On the other hand we are supposed to believe that all Astra math results with no independent peer review are correct. The Lean proofs are tens of thousands of lines long with no comments where the main theorem even is.
The ambitious AI could have inserted another obfuscated proof of False or hidden False in the hypotheses of the main theorem, wherever that is.
Lean, due to its advanced features, has had the most of soundness bugs of all provers:
The semiconductor industry uses ACL2 or HOL-light.
- xelxebar
Intriguingly, Metamath handles recursive definitions by factoring out the recursion into a single higher-order function:
https://us.metamath.org/mpeuni/df-rdg.html
Essentially, it's just doing a lazy fixpoint a la Haskell's fix function. The definition is a little more general, though, to make it work for both transfinite and well-founded recursions as well.
This chashed out nicely in a sequence builder:
https://us.metamath.org/mpeuni/df-seq.html
which specializes to "normal" recursion.
- monocasa
Previous related discussion: https://news.ycombinator.com/item?id=49137060