Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.

Sign up to join this community
Anybody can ask a question
Anybody can answer
The best answers are voted up and rise to the top

Explore our Questions

10 votes
1 answer
157 views

Is there a Mizar-like sublanguage for Coq?

11 votes
0 answers
153 views

Is there a proof assistant (or an embedding) for the (co)end calculus?

5 votes
0 answers
69 views

Is any theorem prover able to prove quadratization relations without knowing the proof strategy that humans used?

31 votes
2 answers
2k views

What work has been done on computationally intensive proofs?

13 votes
2 answers
173 views

Tools for checking the consistency of a type theory

9 votes
1 answer
155 views

Generating valid statements without a proof goal

3 votes
1 answer
91 views

List of general purpose Coq sublanguages for defining custom tactics

12 votes
4 answers
260 views

What games are there?

15 votes
2 answers
157 views

Are there any proof assistants or theorem provers based on the method of analytic tableaux?

5 votes
1 answer
99 views

Libraries of formally stated theorems with proofs verified by humans

14 votes
1 answer
179 views

Are there automated theorem provers for constructive logics? What strategy do they use?

5 votes
2 answers
136 views

Are there any provers based on a paraconsistent logic?

11 votes
2 answers
127 views

verifying combinatorial constructions - choice of a proof assistant

14 votes
4 answers
163 views

Proof Assistants with support for creating executable software artifacts

Browse more Questions