Tag
A hands-on blog post comparing four theorem provers—Lean, Isabelle/HOL, HOL4, and Agda—by formalizing Euclid's proof of the infinitude of primes in each, with opinionated rankings on usability, interactivity, and enjoyment.