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:
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.
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.
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"
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.
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.
In HOL Light? Just so you can run the proof objects through another prover like Isabelle. Wasn't that your original ambition?
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)
> So you get complex recursion and inductive definitions baked into the kernel.
It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.
In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.
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.
Isabelle is actually a "logical framework", so it supports intuitionistic logic, actually its meta theory is intuitionistic higher-order logic.
So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.
> 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.
I mean it's an old term in algebra/analytics that predates sytem-kernels by 50 years or so. And even in the meaning compute/solver/gpu-kernel, even thuough predated by systems kernel, it has still been in use at least 30 years.
So proof kernel is not that far fetched, I think. I only skimmed the article though ... so not saying if it was good use here or not.
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 is apparently equivalent to having more axioms) and that results in a greater risk of having bugs in the proof checker itself.
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.
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.
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:
https://cr.yp.to/proofs.html
The semiconductor industry uses ACL2 or HOL-light.
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.
As you know, Rocq and Lean folk want more than just that from their proof objects. They want proofs to contain executable code, often of the very programs they were verifying, and so treat their proof assistants like programming languages with verifiers attached. So you get complex recursion and inductive definitions baked into the kernel. Whether this is a good idea or not is obviously pretty disputed among us, though I'm mostly with you and Larry :)
It is a pragmatic choice, just like a type system is. I think both of these choices are outdated now that formalisation is fast. What you really want is a simple semantics (what is the semantics of Lean again...?), and build on top of that by verified kernel extensions. Program extraction via proof objects doesn't really work, I don't think anyone does that for real. What you do is you write your program in your term language, and export the meaning of that term as a program. Isabelle does that, too, and you don't need proof objects for that.
In my current version of Practal (Practal Zero) I have a switch for keeping proof objects around as well, in case I want to maybe transform proofs in some reuse scenario. Not sure if I will actually use that, ever, because it would be slow, too. Also, I would rather prove that a certain transformation is correct, and then add this as a kernel extension.
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.
So this is not because of the logic, it is because of the mindset. Intuitionistic logic is usually championed by people who want to emphasise computation over reasoning, and that is why they build computation as one their reasoning steps into their kernel. They don't have to do that. They do it deliberately, because it aligns with what they like, and how they like to think about logic.
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.
Likewise "harness" can be used to mean "to collect and control something so that it can be used effectively".
So proof kernel is not that far fetched, I think. I only skimmed the article though ... so not saying if it was good use here or not.
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.
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.