Comparison of Proof Assistants for the Physics Derivation Graph

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.

Rocq

https://en.wikipedia.org/wiki/Rocq

Lean

HOL

HOL Light theorem prover

HOL Light tutorial

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

Isabelle

https://en.wikipedia.org/wiki/Isabelle_(proof_assistant)

https://isabelle.in.tum.de/