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.
compsci
language
networks
stringology
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