A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda
In which I compare Lean, Isabelle/HOL, Agda, and HOL4 with only mild regard for "fairness". All four of the above are theorem proving applications; that is, their purpose is to computer-formalize mathematics. Broadly speaking, both Lean and Agda are dependent-types based systems, utilizing the Curry-Howard correspondence to prove theorems via a complex type system, whereas Isabelle/HOL and HOL4 are LCF-style systems, with a small "proof kernel" containing base rules (e.g. ) that all proofs must be constructed via. Both foundations have advantages and disadvantages, and some will be discussed. I have formalized in all four a proof of the infinitude of primes; that is, the statement "For any number n, there is a prime larger than n". The exact proof formalized is the "usual" construction by Euclid, which you can find on Wikipedia if you want; see here . All of the proofs structurally look similar (mostly, we'll get to that), and hence it was the user experience that made the difference. For transparency, before this experiment, I was most familiar with Isabelle/HOL and Agda, and to some extent learnt HOL4 and Lean as part of this review. What follows is a bunch of opinions and somewhat arbitrary categories. Don't expect an unbiased review, please. If you only want proof comparisons, skip to Proof Comparisons, and if you only want more opinions, read the below and then skip to Arbitrary Rankings. The opinions go first. I do not claim any of the following proofs are perfect! They're probably quite mediocre, really. There are a few categories by which we can group these theorem provers. We have the above mentioned: But there's also: Reasoning: Both Isabelle/HOL and Lean provide "live updates" as you type, and their structured proofs can be "down-arrow"'d through, to see intermediate steps. In contrast, both completed HOL4 and Agda proofs exist as fully-put-together terms that must be manually taken apart if you wish to inspect their internals. Both HOL4 and Agda can show you your current state and related information at any time, of course. Isabelle/HOL has , which calls out to a number of external proof generation methods (SAT/SMT solvers, various FOL solvers, etc). For any goal that looks doable-but-annoying, there's a solid chance can solve it - this is nice because it saves you work, but the proofs it generates are also indecipherable, which is perhaps less than ideal. There also exists an equivalent for HOL4 called HolyHammer, but I didn't realize it existed until after I was writing this. Oh well. Isabelle/HOL and HOL4 both have very good support for many automated simplification and proof methods, which come in quite handy when trying to work with complex assumptions, for example. It may not be obvious how to proceed without simplification kicking in to chunk everything down. Lean has decent automation, but not to the same level as Isabelle/HOL or HOL4. Its is not nearly as productive, and while is a very neat approach that can sometimes rival , a lot of the time it's quite useless for reasons beyond me. Both and are all-or-nothing; if they don't solve the goal, they make no progress. This is in contrast to (in all three), or more specialized tools like (Isabelle/HOL) or (HOL4), which can make some progress and then leave the context in (ideally) a better place. The fact Lean doesn't have nearly as good partial-automation is a bit of a shame, because in my experience that's what actually matters more. Notably, both Lean and Isabelle/HOL have a (In Isabelle/HOL, / for with/without ; in Lean, / / ) that "have a go" at your goal with various automated methods and direct solve attempts. HOL4 doesn't have an equivalent, as far as I can tell, which is unfortunate, as it's quite handy. Agda has essentially no automation. The only simplification you get is what can be computed based on inputs to functions. This, to be a bit frank, sort of sucks. It's quite hard to get things done because there's so much manual fiddling that must be taken into account. I am personally not a fan. Isabelle/HOL and HOL4 are both extremely classical in their foundations, which means that they accept the Law of Excluded Middle (∀ P. ¬P ∨ P), and both also axiomatize Hilbert's epsilon, which leads also to the Axiom of Choice. This seems to have a very positive effect on automated solvers, which quite often rely on laws such as double-negation elimination (¬¬P --> P), which is equivalent to the LEM. Lean is theoretically constructive (and hence does not have the LEM by default), but some of the "good" proof automation requires the LEM, and it seems the norm to use Lean classically, so that's what I did. for example just assumes you're using it. This does have the disadvantage that Lean isn't as good at dealing with e.g. existentials, for example. Agda is constructive by default, and it seems the norm in the Agda world to keep your proofs that way, so I did. The big advantage of this is that after proving there are infinitely many primes, I can actually generate them! I can give my proof a number, and it'll spit out a prime bigger than that number. The disadvantage is that it is horribly slow to do so: This may make sense if you looked at the proof structure above; we consider , so inside that proof, it's checking primality at numbers around ~360,000; that's going to be a bit slow. This construction, it should be noted, isn't meant to be fast, but it's also the most natural one. Is it worth giving up the LEM and good proof automation? You decide. I'm more a fan of LCF because it seems more amenable to automation, and I don't see the point of carrying around proof terms (classical logic is too useful!). If you vehemently disagree, email me at contact AT blueberrywren.dev, and if I like your argument enough I'll post it here. Both Lean and Isabelle/HOL are interacted with interactively. Lean has modes for other editors, but high recommends the use of VSCode, and Isabelle/HOL has its own editor (jEdit) that it also practically forces the use of. This is fine ; I understand why they do this, as interactive development is reasonably hard to make generic. Both of them make it work. HOL4 is interacted with via either an Emacs mode or a Vim mode, and keybinds that allow one to copy text in/out of a running HOL4 REPL. This sounds weird because it is, but it works surprisingly well. I was already an Emacs user, so nothing really changed for me. Agda is also interacted with via an Emacs mode, but everything happens in your file; you can use keybinds to refresh the state, add proof goals, etc. It also works fine. As mentioned above, the advantage of the Lean/Isabelle/HOL approach is that one can see proofs in-progress, which you can't with Agda. Both Isabelle/HOL and HOL4 have extremely good mechanisms for searching for theorems; an editor panel + for the former, and / for the latter. These allow for the searching of theorems by both name and by patterns, so I could for example search for lemmas of form . This is so handy! Very often you know the shape of something you want, but maybe not the lemma itself. Lean has leansearch and loogle, which are interesting, but they: Which kind of sucks. and exist as "here's stuff you might be able to do", but they're nowhere near as flexible. Agda, as expected perhaps, does not have an equivalent. One must become a master of zen looking through the right parts of the Agda standard library. Note: This isn't really meant to be a tutorial for any of these, though I will do a little explaining at the start. It's mostly for the reader to compare them, and see what ~equivalent statement proofs look like in different languages. Let's get into the proofs! We'll go segment by segment, exploring sections of the proof and explaining as we go. Before that, some vaguely interesting stats: These are nowhere near apples-to-apples, but they're still fun. We start with defining divisibility. In Agda we cheat and use the standard library version, so we can get proofs around computing divisors, which I didn't feel like redoing. Isabelle/HOL: Agda (looks like, in the standard library): So, basically the same. Then there's a few lemmas around divisibility proved ( , , etc). One we'll show off is , as it's mildly interesting in some of the theorem provers. In all of the following, the mult/sub lemma essentially states . Isabelle/HOL: The proof search procedure does most of the work. We do some unpacking, then identify as the other term (such that ). Then grind with the appropriate lemma gets us there. Like Isabelle/HOL, when supplied with the appropriate lemmas, takes it out. Very similar. is an abbreviation for , and like in Lean, we must manually point out . It was interesting to me that the Lean proof was, to some extent, such a pain. I had to put more effort into that one than any of the others, despite Lean having reasonably decent automation! Finding the appropriate lemmas was mildly more painful, and this was while I was still puzzling over syntax, to be fair. We next need to define the product of a list of numbers, which looks like the following: Isabelle/HOL: The and markers were meant to help the automated proof methods out, and they did! Defining things in HOL4 is a little interesting, because you're just defining the body as a proof! That definition spits out a theorem that is literally Here in the Agda proof we also do a bunch of work to set up what will become a decision procedure for primality. This is because later we wish to ask "Is this prime?", and without the LEM to say "It must either be prime or not prime", we need to write an algorithm to decide this for us. Back on track, we need to show a few lemmas around with prod list function. One of the interesting ones is as follows, where we prove that a number in said list will divide the product of the list. Isabelle/HOL: Very implicit; it's hard to tell what's going on, but the basic structure is there. Induct on the list, do some casing, apply a lemma about . Reasonably large. We have to destructure the membership quite manually, which gets a little troublesome. It's a fairly straightforward proof, though. Also not crazy, although it's hard to see the exact structure without comments (which I didn't write :P). This is a good time to point out HOL4 proofs are literally just SML terms! There's nothing more to it! The combinators and (for apply latter to all subgoals of former, and to one subgoal of former resp.) are just infix functions composing other functions! It's all just SML! You interact with HOL4 through a REPL, so you construct stuff dynamically, but then you have to puzzle piece your function together afterwards. Once you know that, it's more obvious what's going on; we induct, handle the first case, then simplification on give us two goals ( and resp.) Very explicit, but also quite concise. Matching on the list membership is quite intuitive, because the Agda mode in Emacs includes a command to automatically case split on basically everything. While it's much more implicit in Isabelle/HOL and HOL4 (a common theme), all four of these proofs take the form of asking whether the value we care about is at the head of the list, or somewhere later on, and that decides what we fill in divisibility with. Then, Primality! Isabelle/HOL: In Agda we also define what it means to be composite as a "positive" definition, instead of just "not prime"; this makes working with it quite a bit easier. The next "interesting" proof is proving that every not-prime number greater than one has a prime factor. In Agda this is part of the definition of being composite, so we don't bother including it. We're going to move slightly faster from now on, so I won't explain each snippet. Just compare yourselves. Isabelle/HOL: The steps of ~> and ~> in the HOL4 one annoyed me a lot, but I couldn't figure out how to golf them down. Similarly, this line: of the Lean proof causes me pain. We're almost there now! Two more steps to go: Prove there's always a prime outside a given set (list) of numbers, and use that to show the final statement. First, the former: Isabelle/HOL: The Agda proof differs slightly to accommodate the lack of ranges later. The Isabelle/HOL proof clearly wins in terms of length here, but it's also really unclear what's going on. Everyone else gets progressively more verbose, and the HOL4 proof in particular here is a bit nastily nested. (a first-order solver) does a lot of heavy lifting, as does . If you're wondering why both Isabelle/HOL and HOL4 have something named / , it's because it was ported to Isabelle/HOL from HOL4. We arrive at our final statement! Agda requires some more fiddling as it doesn't have ranges built in like the other two do, but we use our lemma above to construct the list , and then show there's a prime outside that (and that it hence must be above ). Isabelle/HOL: It annoys me I couldn't get this smaller, but oh well. We've done it! Euclid would be proud. (probably) It's now time for more opinions! I have five criteria I'll be ranking on: Not much to comment on here, really. is a great boon, and both Isabelle/HOL and HOL4's theorem discovery tools are great. Lean was reasonably close behind, with often giving good related lemmas as a solve, and Agda was clearly last. Paging through files online to find lemmas is annoying. Love it or hate it, Agda being entirely raw proof terms means things are essentially exactly what you tell them to be. There's never a moment where you're going "Damn, why won't the simplifier just expand this but not that!". Lean is pretty good here, as it's quite conservative around what it chooses to manipulate and everything is explicitly named. HOL4 has a pretty reasonable learning curve as one learns to use things like that can target based on patterns (e.g. ), but once you figure it out it's not bad. Isabelle/HOL really isn't stunning here; it's often hard to get it to do exactly what you want. I had a great time learning both HOL4 and Lean, but HOL4 edges out because it's such a unique interaction mode and it's still very powerful. Lean was fun, although annoying at some times, and Isabelle/HOL wasn't particularly interesting, but some of that is because i'm familiar with it. Agda sort of sucked at times; writing a whole primality decision procedure and fiddling with type nonsense got quite annoying after a while. Agda "wins" for the same reasons as above. Having to do really manual proof search and fiddling constantly wasn't super pleasant. HOL4 and Lean both had their own annoyances and I think it's unfair to rank one over the other; the learning curve on assumption manipulation / sim was quite significant in HOL4 and Lean's automated tools were finicky enough it quite sucked at times. Isabelle/HOL i'm just used to, so there's some bias there. Same reasons as above; there were a lot of times where HOL4 just had me going "huh????" because some theorem-tactic wasn't doing what I expected it to, or was transforming the goal in an unpredictable way. Lean had similar, where it would just randomly decide "erm actually i'm not going to solve this really simple goal for you with do it yourself please" in ways that left me baffled. Seriously, sometimes is smarter than and sometimes it's stupider than . Weird. Isabelle/HOL had some of the same but was generally fine, and Agda was utterly predictable. HOL4! I had a great time learning it, it's a seriously interesting system. I didn't not enjoy Lean, but there's enough odd stuff going on to make me slightly wary of it, I suppose. Isabelle/HOL remains the one I'm best at (I am somewhat paid to write it, so that helps), and Agda is Agda. What should you try? Well, all of them, but I would at least try out something new. If you've only used dependent theorem provers before, try Isabelle/HOL or HOL4, and vice versa. If you've only used theorem provers that work fully interactively like Lean, try HOL4 or Agda! New experiences are the joys of life. Isabelle/HOL: LCF-style: Isabelle/HOL, HOL4 Dependent-style: Lean, Agda High-interactivity: Isabelle/HOL, Lean Low-interactivity: HOL4, Agda High-automation: Isabelle/HOL, HOL4 Medium-automation: Lean Low-automation: Agda 0: 2 (instant) 1: 3 (instant) 2: 7 (instant) 3: 5 (instant) 4: 11 (quarter second) 5: 7 (quarter second) 7: 61 (10s) 8: 19 (40s) Aren't built in. Aren't as good. Isabelle/HOL: 117 LOC, with 19 proofs. Lean: 155 LOC, with 12 proofs. HOL4: 190 LOC, with 16 proofs. Agda: 264 LOC, with 45 proofs (29, not counting blocks) Ease of proof discovery (how easy is it to figure out what I want to do) Ease of proof manipulation (how easy is it to do what I want) Enjoyment (how much fun did I have) Annoyance factor (how often was I going "ugh!") Puzzled factor (how often did I go "why can't you solve this??") Isabelle/HOL Isabelle/HOL Isabelle/HOL HOL4 / Lean (tied second) Isabelle/HOL Isabelle/HOL
Programming
Tutorial
Shell
Backend
C++
Rust
JavaScript
Security
AI
Career