Proof assistant
https://en.wikipedia.org/wiki/Proof_assistant
Hol4
https://hol-theorem-prover.org/
Moscow ML
Hol Light
https://www.cl.cam.ac.uk/~jrh13/hol-light/
OCaml
Lean
https://leanprover.github.io/
C++, Lean
Microsoft
Metamath
https://us.metamath.org/
C
Mizar
http://mizar.org/
Pascal
Coq
https://coq.inria.fr/
OCaml
Isabelle
https://isabelle.in.tum.de/
Standard ML, Scala
Idris
https://www.idris-lang.org/
Idris
Plato
https://github.com/ksrky/Plato
#数学基礎論