Proof assistants
Automated theorem provers
2019-12-08 — 2022-08-08
Wherein a Particular Slant on Computational Symbolic Mathematics for Foundational Applications Is Described, and the Lean Proof Assistant Is Noted to Provide a VS Code Interface for Formal Theorem Development.
A particular slant on computational symbolic mathematics targeting foundational applications.
Proof assistant helps us to prove theorems. See Proof Assistants Stack Exchange for some action research.
1 Lean
The most active community AFAICT. Open source. VS Code interface (!).
2 Coq
The previous king
3 Naproche
Naproche is a naturalproof assistant that models the usual reading and checking of mathematical proofs by mathematicians. The naturality of Naproche is twofold: it uses a controlled natural language as its input language, but it also aims for proofs free from clutter and tedious details, i.e., proofs that read naturally to mathematicians. The input language of Naproche is embedded into LaTeX, allowing users to combine natural argumentative language with symbolic material in a manner that is familiar to mathematicians.