Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- 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.
by inigyou - 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 is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
by brazzy - The bigger the kernel gets, the more stuff you gotta hope is bug-free.
I'd rather keep it small and deal with the extra work somewhere else.
- Previous related discussion: https://news.ycombinator.com/item?id=49137060by monocasa
- 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.
by xelxebar - 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.
by f12a8h - Here is the postmortem of the lean bug: https://leodemoura.github.io/blog/2026-8-1-postmortem-for-ke...by red_trumpet
- 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 without knowing what other measures are in place to assure the integrity of the distribution.by ajb
- 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.by yjftsjthsd-h
- > 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.
by wseqyrku - Hey, it's been awhile since we had a good microkernels vs monolithic debate. Time to post it!by phendrenad2
- Pretty much. The kernel of a proof assistant is the absolutely trusted core, and ultimately gets to decide what is or isn't a proven mathematical fact (so roughly a kernel resource). Over that, you build a huge amount of (userspace) tooling that doesn't have to be absolutely trusted since its job is just to talk into the kernel and get theorems.
A kernel bug manifests as the kernel deciding that something is a theorem which shouldn't be. The worst case is when it decides that False is a theorem, from which it immediately follows that absolutely everything is a theorem.
The HOL Light kernel (mentioned in the article) is about 500 lines from one file (https://github.com/jrh13/hol-light/blob/master/fusion.ml), and is a very straightforward implementation of a simple type theory (https://en.wikipedia.org/wiki/HOL_Light#Logical_foundations). I'm not so familiar with Lean, but it would appear its kernel is spread over this C++ directory: https://github.com/leanprover/lean4/tree/master/src/kernel.
As mentioned in the article, HOL Light gets away with a lot because it only cares about delivering theorems. Other systems want to retain the proofs as artifacts (sometimes called certificates), and once you do that, you need to make sure these artifacts aren't stupidly huge or otherwise useless. Provers such as Rocq (and I assume Lean) additionally want their proof objects to contain decent executable algorithms backing the proof.
HOL Light also does pretty much no evaluation. The most it understands of evaluation is that (λx. f) x = f. If you want to evaluate anything more complex than this, you build that in "userspace" and you do all the equational reasoning manually via the kernel.
Lean and Rocq kernels do full evaluation of recursive functions, so they have to come installed with an API for building those recursive functions and internal checking to make sure those functions are terminating. The article's author is asking whether you could redo something like Lean and Rocq where the recursive function API was much simpler. I've wondered for a while whether you could also have the evaluator as basic as HOL Light's, and do the rest in userspace. I think there were theorem provers like this that went out of fashion decades ago.
It used to be a much more exciting space before Lean somehow got everyone's attention. The author is the co-creator of Isabelle/HOL, and is still not sure why there is so much more excitement for Lean than for simple type theory.
by momentoftop - I think in the background of article's premises is an argument about classical vs. intuitionistic logic, rather than only about the merits of putting stuff in the kernel vs. outside.
Isabelle seems to use classical logic and set theory. Classical logic is often simpler, but when you do the "hard toil" (as the article puts it) of building recursive functions on set theory, all you've really done is to nonconstructively prove the existence of a set of pairs with certain properties. Good luck evaluating such an abstract "existence" with any concrete argument. Whereas intuitionistic logic as used by Coq is more complicated, but that's in part because its notion of "function" is an actual procedure in your computer that can accept an argument and produce a result.
At least that's to the best of my understanding; it's been a while since I have looked at any of this, so feel free to make corrections.
by codeflo - Yes, the analogy might help. Though as far as I know the common OS kernel reply 'we have to stick it all in the kernel to achieve performance' doesn't apply to proof assistants.by eru
- Ha, I actually wrote a paper pushing on this "kernel" pun between OSs and proof-checkers [1], designing a HOL kernel structured like an OS kernel.
[1]: https://drops.dagstuhl.de/storage/00lipics/lipics-vol269-typ...
by dmulligan