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

4 votes
1 answer
116 views

Can we completely erase propositions in the type checker?

3 votes
1 answer
119 views

Equality type and Propositions

0 votes
2 answers
107 views

Coproducts in Lean

1 vote
2 answers
54 views

Suppressing notation in Lean

1 vote
1 answer
69 views

Inductive types associated to instances of a structure in Lean

1 vote
1 answer
76 views

Making a finite graph type in Lean - introduction rule

5 votes
1 answer
97 views

In lean, how do I expand a definition without knowing what it is?

1 vote
2 answers
83 views

In lean, how to work around "invalid pattern, 'x' already appeared in this pattern"

3 votes
2 answers
332 views

In lean, why is it possible to prove zero_ne_succ (without adding it as an axiom) by using pattern matching?

8 votes
2 answers
288 views

Learning Math Proof via Proof Assistants

7 votes
1 answer
195 views

Cardinality of Type in a given universe

5 votes
0 answers
191 views

An algorithm for the substitution of formulas for predicates in first order logic

5 votes
1 answer
84 views

What are the differences between theorem, example, def, etc?

4 votes
1 answer
87 views

How to prove a property of a conditional statement without using tactics in Lean?

Browse more Questions