Why is it all in the kernel?
[general Lean Isabelle HOL system philosophy memories Sensational news! The Collatz conjecture has just been refuted. Ramana Kumar has proved its negation. The proof has been checked in Lean and double‑checked using the independent Nanoda type checker. Unfortunately, the proof is wrong. It exploited a bug in the Lean kernel. Somehow, Nanoda didn’t detect the error either. Now I am not writing to gloat about this. Soundness bugs have been discovered in Isabelle, among many other proof assistants; for all I know, a new and monstrous bug will be discovered tomorrow. Nevertheless, there are some lessons here, so let’s go!
The Collatz conjecture
This famous conjecture has been around for nearly a century, attracting the attention of serious mathematicians and cranks alike. It concerns the following procedure. Start with a number N. Now repeat this step: if N is even then divide it by two; if odd, set N to 3N+1. Collatz conjectured that this procedure is guaranteed to reach 1 no matter what value of N we start with. Extensive testing has failed to find a single counterexample. Recent work shows language models to be quite good at finding counterexamples to conjectures, so why not Collatz? Resolving it really would cause a sensation.
The dead weight of proof objects
As we have known for half a century, proof objects are unnecessary. Robin Milner designed the ML language for the specific purpose of supporting proof assistants. Through the notion of an abstract type, the proof kernel could be made secure from the rest of the program. The rules of inference, confined to the abstract type, would be an API for creating theorems.
Nevertheless, much of our community has doubled down on storing proof objects. In particular, they noted that a proof object was a certificate that could be checked independently. But I am not aware of a single instance where an independent proof checker detected a soundness error that had passed through the kernel of a proof assistant. For Collatz, as we have seen, Nanoda was also fooled. When we consider the memory burden that proof objects represent, this is analogous to driving everywhere pulling a spare car on a trailer behind you in case of a breakdown. And your car does break down, but lo and behold, the spare car doesn’t work either. And the exact reason your car broke down was the burden of pulling the spare car. Because it is only the proof calculi that have proof objects that seemingly need to put everything into the kernel.
Theft versus honest toil
For most of the 20th century, logicians assumed the fewest axioms they could, from them deriving the rest of mathematics. Possibly they were worried about Russell’s and other paradoxes; possibly they were just parsimonious. This point of view was perhaps best put by Russell himself:
The method of ‘postulating’ what we want has many advantages; they are the same as the advantages of theft over honest toil. Let us leave them to others and proceed with our honest toil. (Russell, 1919)
So it’s notable that – so rumor has it – the bug in Lean was caused by nested inductive types in the kernel. A number of soundness bugs in Rocq were caused by pattern matching involving recursive functions in the kernel. I’m not precisely sure why dependent type theories are not expressive enough to express things like recursion from a more basic calculus. The reason is probably technical. But let’s be clear: in set theory and in simple type theory, you have to assume very little. Set theory gives you a few principles for introducing sets: unions, separation, pairing, replacement. Simple type theory gives you a little bit of logic and a bit of λ-calculus, which gives you a typed set theory where the sets are Boolean-valued functions. Then, with honest toil, you can obtain inductive definitions, records, recursive data structures and recursive functions in quite general settings, including pattern matching and partial functions. You can perform numerical calculations using symbolic binary arithmetic. Because all these things are defined in terms of the primitive axioms, rather than being postulated, they lie outside the kernel and cannot lead to contradictions.
Back in the 1980s, when I was working with Martin‑Löf type theory, a question arose about expressing recursive functions. The theory only recognized forms of primitive recursion. But the theory also admitted higher types, giving the possibility of more powerful forms of recursion. Having learned mathematics in the tradition of honest toil, I worked (and it really was laborious) to define a system of combinators within Martin‑Löf type theory that could express a vast space of terminating recursive functions. But I hadn’t understood how this game was played. The correct answer to the question was to extend MLTT with a general notion of recursion, and I must admit, it could be done simply and elegantly. I’m not sure anyone ever understood what I did. Years later, I saw the paper cited with the comment, “Paulson extended MLTT with recursion”: they couldn’t imagine someone obtaining recursion through honest toil.
What does the honest toil look like?
I can see why the implementers of a proof assistant take the option of theft, because the honest toil really is like breaking rocks. The easiest of the many objectives is recursive data structures. An inductive definition can be transformed into a monotone operator on sets. The least fixed point gives you an inductive definition, and if you prefer a co-inductive definition, you take the greatest fixed point. In Isabelle, we seldom bother to link these constructions to types, but recursive data types are an important special case, now handled in a general and sophisticated way through bounded natural functors.
The construction of recursive functions from first principles is particularly tedious. You begin with a well‑founded relation and prove the existence of the desired recursive function by well‑founded induction. The work I did on recursion in MLTT was somewhat helpful in this, so it was not entirely wasted. Isabelle/HOL now supports recursive function definitions in great generality, including pattern matching and termination checking. And all of these things lie safely outside the kernel.
There’s an irony that proof objects are sometimes touted as leading to greater soundness guarantees. The opposite is clearly true. If soundness is your main concern, you should go for HOL Light or HOL4. Isabelle has had more bugs than those, but few, and definitely far fewer than certain other systems.