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

3 votes
0 answers
81 views

Recursive notations with forall quantifier

2 votes
0 answers
46 views

SSReflect tuple constructor: why not use phantom?

3 votes
0 answers
55 views

Unfolding expressions in Coq by one layer

2 votes
4 answers
195 views

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

12 votes
0 answers
147 views

How do Coq's bidirectionality hints (`&`) affect type checking?

11 votes
3 answers
587 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

13 votes
3 answers
647 views

How to extract the witness from exists in Coq in function notation/without destructing?

3 votes
1 answer
133 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

4 votes
0 answers
67 views

Display style proofs using Coq

4 votes
0 answers
49 views

Tactic unification vs evarconv in Coq

10 votes
1 answer
157 views

Is there a Mizar-like sublanguage for Coq?

9 votes
1 answer
531 views

What axioms do I need to search the naturals?

3 votes
3 answers
426 views

How can I prove this theorem with induction in Coq?

5 votes
0 answers
86 views

Prove equality in a record type

Browse more Questions