21–30 of 43 posts
Earlier quoted context omitted.
Yeah in theorem provers usually the opposite is true: "We want to put as little stuff as possible in the kernel because that's the part we need to verify by hand"
In an OS kernel that instinct is also true: 'we want to put as little as possible in the OS kernel, because that stuff can bring down the machine.'
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinction between two kinds of things - "objects" and "types" - and then argue which one is better. No, I don't speak Lisp. And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
> Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel.
I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
Earlier quoted context omitted.
In an OS kernel that instinct is also true: 'we want to put as little as possible in the OS kernel, because that stuff can bring down the machine.'
That isn't true, as there are many things that can bring down the machine. If your X or Wayland server crashes, it brings down your machine.
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.
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…
Earlier quoted context omitted.
That isn't true, as there are many things that can bring down the machine. If your X or Wayland server crashes, it brings down your machine.
It doesn't, it just loses your session
Earlier quoted context omitted.
> Proof assistant kernel, not operating system kernel It's the neologism they use to own the word and define it however they want. The other one is 'harness' that I didn't even click to see what they want it to mean.
The word kernel always meant "the most important part of something". Likewise "harness" can be used to mean "to collect and control something so that it can be used effectively".
The debate over proof objects versus proof types seems particularly ivory-tower, since it's all just data being processed by a computer. You invent this distinction between two kinds of things - "objects" and "types" - and then argue which one is better. No, I don't speak Lisp. And you don't "throw away proofs" when using proof types. They are right there in the theory file if you want to check them again.
I have to admit that I know very little about formalized proofs, but the article seems to put some reasoning behind this distinction, specifically this statement: > Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel. I interpret that to mean that for some reason, having proof objects requires or at least encourages putting more logic in the kernel (which…
As I understand their writing, ML is a language meant for developing proof assistants and this debate is specific to proof assistants written in ML, about the extent to which you use ML's type system as part of the kernel (proofs or theorems are types, at least partially), or write one yourself (proofs are just objects).
Even Rust has an unsound type system that allows arbitrary memory access in safe code, so you can't just assume your programming language has a sound type system.
Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...
The one thing that gives me concern in their is "nanoda [the external proof checker] is [now] tracked daily". Although that would have caught this issue, we also now live in a world in which some model is going to think that hacking the proof-checker distribution is the obvious way to obtain the proof it is after; I expect that attempts on that will be much more common than soundness bugs. However, this is said witho…
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.
[1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...