navigation / documentation overview / design choices / proof assistant comparison
Recommendation: Read the user documentation and FAQ first. This page assumes familiarity with the jargon used in the Physics Derivation Graph.
What constitutes a viable proof assistant option? Cited by a journal like Annals of Formalized Mathematics,
"Examples of popular proof assistants include Agda, Rocq, HOL Light, Isabelle, Lean, and Mizar."
| Aspect | Agda | Rocq | HOL Light | Isabelle | Lean | Mizar |
|---|---|---|---|---|---|---|
| wikipedia page | Agda | Rocq | HOL Light | Isabelle | Lean | Mizar |
| Primary Community | Computer scientists, Programming Language (PL) researchers, HoTT theorists. | Large mix of industry (software verification) and academic mathematicians. | Hardware verification specialists and extreme minimalists. | Computer science departments and formal methods researchers. | Working research mathematicians and "Mathlib" contributors. | Traditional mathematicians focused on a human-readable library. |
| Foundational Logic | Dependent Type Theory (DTT) / Constructive. | Calculus of Inductive Constructions (CIC). | Higher-Order Logic (Simple Type Theory). | Higher-Order Logic (built on a meta-logic). | Dependent Type Theory (similar to Rocq). | Tarski-Grothendieck Set Theory. |
| Strengths | Beautiful syntax; "Programs are Proofs"; excellent for Homotopy Type Theory. | Powerful tactic engine; highly stable; massive industry track record (e.g., CompCert). | Extremely small, trustworthy kernel; very fast execution of simple proofs. | "Sledgehammer" (powerful automation); very readable proof scripts (Isar syntax). | Unified, massive math library (mathlib); excellent VS Code integration; fast-growing. | Human-readable language style; the oldest continuous math library (MML). |
| Weaknesses | Lacks the heavy automation/tactics found in Isabelle or Rocq. | Steep learning curve; legacy fragmentation across 30 years of development. | Sparse user interface; requires OCaml proficiency; less automated than Isabelle. | The "Logic of Choice" (HOL) is not constructive; heavy resource usage. | Rapid version changes (transitioning to Lean 4 was difficult); heavy RAM requirements. | Hard to extend; lacks modern IDE features; rigid structure for new users. |
| Math Coverage | Strong in Category Theory, Type Theory, and Logic. | Broad coverage; famous for Feit-Thompson (Group Theory) and Four Color Theorem. | Very deep in Analysis and Geometry (famous for the Flyspeck Project). | Massive "Archive of Formal Proofs" (AFP) covering diverse undergraduate/graduate math. | Modern research math (Perfectoid spaces, Liquid Tensor Experiment, Algebra). | Extensive library (MML) covering a wide range of classical mathematics. |
| Automation Style | Mostly manual/structural; relies on "interactive editing" via Emacs. | Ltac tactic language allows users to write custom automation scripts. | Manual tactic application via OCaml prompts. | Excellent: Sledgehammer connects to external solvers (Z3, Vampire, E). | Strong: "Aesop" and "Tactic" frameworks; growing AI/LLM integration. | The "Checker" automatically fills in "obvious" gaps between steps. |
| Library Philosophy | Decentralized; standard library is separate from specialized research. | Decentralized; many independent packages managed via Opam. | Monolithic: Centered around a core set of files used by the community. | The AFP (Archive of Formal Proofs) acts as a curated journal for libraries. | Hyper-centralized: One giant repository (mathlib) that keeps everything in sync. | Monolithic: The Mizar Mathematical Library (MML) is a single, integrated body. |
Prompt to Gemini 3 Flash on 2026-03-05:
Create an HTML table that has, as columns, Agda, Rocq, HOL Light, Isabelle, Lean, and Mizar. The rows should have aspects that compare the proof assistants. Example comparisons might include - which communities is the proof assistant popular with? - strengths and weaknesses - what aspects of math are covered? Come up with additional rows for comparison and fill in the table with an assessment.
https://hub.docker.com/r/lcdoutlet/hol-light/
An attempted Docker image: https://github.com/allofphysicsgraph/proofofconcept/blob/gh-pages/sandbox/docker_images/ocaml_alipne_with_hol_works/Dockerfile
and https://github.com/allofphysicsgraph/proofofconcept/blob/gh-pages/sandbox/docker_images/ocaml_alpine_with_HOL/Dockerfile