The author compares four theorem provers (Isabelle/HOL, Lean, HOL4, Agda) by formalizing the same Euclidean proof of the infinitude of primes across all four systems. The article contrasts dependent-types-based systems (Lean, Agda) with LCF-style systems (Isabelle/HOL, HOL4) and evaluates user experience across multiple dimensions including ease of proof discovery, manipulation, enjoyment, and annoyance.
Background
The rise of Lean 4 has brought increased attention to theorem proving and formal verification in both academic and industry settings. Comparing different proof assistants helps practitioners choose the right tool for formalizing mathematics and verifying software.
- Source
- Lobsters
- Published
- Oct 9, 2026 at 10:30 PM
- Score
- 6.0 / 10