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

0 votes
2 answers
25 views

Is there a tactic in Coq to make a hypothesis from applying two hypotheses?

2 votes
0 answers
34 views

Coq: can `tauto` be used to prove classical tautologies?

1 vote
1 answer
57 views

reference request for an introduction to higher order logic

6 votes
2 answers
120 views

Defining essentially unique objects with typeclasses

0 votes
1 answer
36 views

Non-dependent implicit argument instantiation in Coq's reference manual does not work

0 votes
1 answer
67 views

A problem similar to intermediate value problem

3 votes
4 answers
479 views

How can I prove this theorem with induction in Coq?

2 votes
0 answers
49 views

Unexpected eta expansion in constant definition

0 votes
1 answer
33 views

Define a function using another function

8 votes
1 answer
196 views

Learning Math Proof via Proof Assistants

1 vote
1 answer
128 views

dependent pattern matching and kind of inversion

5 votes
0 answers
46 views

Graph algorithms in Coq

10 votes
2 answers
511 views

Is coercion to a higher universe injective?

6 votes
1 answer
248 views

What are some good (bad) examples of "green slime"?

Browse more Questions