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

6 votes
1 answer
163 views

How to implement a visual proof assistant?

8 votes
3 answers
256 views

Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?

2 votes
1 answer
123 views

What are references for learning type theory?

2 votes
2 answers
153 views

Reference request for an introduction to higher-order logic

0 votes
0 answers
79 views

Existential variables in dependent type theory

3 votes
0 answers
61 views

Where is the discriminate tactic defined in Coq?

6 votes
1 answer
133 views

What are some good resources for Proof Assistant based exercises/puzzles for recreation and practice?

3 votes
3 answers
110 views

Mechanization of game semantics?

2 votes
1 answer
84 views

Is there any work on the use of free logic in proof assistants?

3 votes
1 answer
68 views

Use of modal logic in metaprogramming

6 votes
3 answers
3k views

What are good examples of April fools jokes in the proving assistant community?

6 votes
1 answer
193 views

Parameterized Datatypes in a Universe à la Tarski?

12 votes
3 answers
255 views

PDEs and proof assistants

19 votes
9 answers
413 views

What are good books for learning about proof assistants for Functional Analysis?

Browse more Questions