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

14 votes
3 answers
719 views

Do you need a Hilbert style Epsilon operator for definitions in set theory?

8 votes
3 answers
511 views

Construction of inductive types "the hard way"

10 votes
0 answers
149 views

Unintentionally proven false theorem with type-in-type outside logic and foundations?

10 votes
1 answer
484 views

What is the role of impredicativity in program extraction?

18 votes
1 answer
817 views

Proof-theoretic comparison table?

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

17 votes
2 answers
326 views

What is the trade-off to accepting impredicative propositions?

29 votes
3 answers
827 views

What are the bases for different Proof Assistants?

4 votes
2 answers
153 views

Can a proof engine be built based on graphs?

15 votes
2 answers
237 views

Are Logics Based on Dependent Types Stronger Than Ones Without?

8 votes
2 answers
170 views

What is the computational complexity of theorem proving?

11 votes
1 answer
145 views

Integration of proof assistants and Wikipedia-like websites?

7 votes
2 answers
189 views

Can the development of proof assistants make mathematicians switch their framework?

Browse more Questions