• Math theorem provers: HOL, HOL Light, Isabelle, Lean, Coq, Metamath, Mizar
  • Theorem proving: have a tree, can be merged into DAGs. Proof search is tree of trees.

    • Lean has a “standard library” called mathlib

    • Hard to formalize proofs

    • Metamath example:

      Untitled

      • It’s a chain of steps, each one transforms the current “state”