A tale of four theorem provers, or: A (reasonably) opinionated comparison of Isabelle/HOL, Lean, HOL4, and Agda
Summary
A personal, opinionated side-by-side comparison of Isabelle/HOL, Lean, HOL4, and Agda as theorem provers. It covers interactivity, automation, foundations, and proof techniques, with concrete code examples and a long 'All the code' appendix. Useful for readers evaluating formal-methods tools and cross-language proof patterns.