Proof assistants

Automated theorem provers

December 9, 2019 — August 9, 2022

compsci
language
networks
stringology
Figure 1

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