The best proof assistants, according to hackers
8 proof assistants recommended in Hacker News comments over the past year, ranked by how many separate people recommend each one.
All proof assistants
- Lean 4A proof assistant and full functional language that pairs well with AI, whose small trusted kernel makes proofs highly reliable; critics cite slow checking and quirky general-purpose use.268recommend
- RocqFree proof assistant for formally verifying programs and math, with a rigorous dependently typed design. Critics say it is mostly academic and Lean has overtaken it.25recommend
- CoqFree theorem prover people use to write machine-checked proofs, praised for rigor and strong tactics. Caveat: proofs are hard to read and maintain, and adoption is limited.24recommend
- AgdaDependently typed proof assistant people prefer for interactive proof checking and math exploration; critics say it is impractical for building ordinary software and has little AI training data.19recommend
- IsabelleMature proof assistant people recommend for rigorous mathematical proofs and software verification. Critics say it is cumbersome for engineering problems and models math functions, not running code.14recommend
- MetamathPeople recommend Metamath for its tiny, simple verifier kernel and the free book that teaches formal proofs. The most common caveat is that its tooling and interface feel archaic.14recommend
- ACL2Free theorem prover, used for industrial verification and recommended as a better fit than Dafny or Lean for reasoning about software. Critics say the user experience is hard to like.6recommend
- Isabelle/HOLRecommended for formal verification because its kernel is small and it has large libraries, and it is seen as a practical alternative to Lean. Critics find the tooling flawed and painful to use.5recommend