Physics Derivation Graph navigation Sign in

Recommendation: Read the user documentation and FAQ first. This page assumes familiarity with the jargon used in the Physics Derivation Graph.

This page compares Computer Algebra Systems (CAS) for use with the Physics Derivation Graph (PDG).

Comparison of Proof Assistants

Lean

HOL Light theorem prover

HOL Light tutorial