A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda

In this analysis, I compare four theorem proving applications: Lean, Isabelle/HOL, Agda, and HOL4. Lean and Agda are based on dependent types and utilize the Curry-Howard correspondence, while Isabelle/HOL and HOL4 follow the LCF-style. All four systems have their advantages and disadvantages. The proofs of the infinitude of primes were formalized in all four systems to examine their user experiences.

Lean and Isabelle/HOL provide live updates as you type, allowing for easy inspection of intermediate proof steps. HOL4 and Agda, on the other hand, present fully constructed proofs that must be manually deconstructed. Isabelle/HOL features Sledgehammer, which can call external proof generation methods, while HOL4 has HolyHammer. Both systems have robust support for automated simplification and proof methods. However, Lean's automation is not as extensive as Isabelle/HOL or HOL4, making Lean's partial automation a drawback.

Isabelle/HOL and HOL4 are classical in their foundations, accepting the Law of Excluded Middle and axiomatizing Hilbert's epsilon, which benefits automated solvers. Lean is theoretically constructive but often used classically to leverage good proof automation. Agda is constructive by default, enabling the generation of prime numbers following a proof.

However, this approach is significantly slower, particularly when checking primality at large numbers. The choice between the different systems ultimately depends on individual preferences and requirements.