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

5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

13 votes
9 answers
408 views

How to represent mathematical partial functions in a type-theory based proof assistant?

3 votes
1 answer
107 views

What are instances of a dependent pair type?

9 votes
1 answer
242 views

Current status of cubical inductive families

14 votes
3 answers
452 views

Bringing OOP features into proof assistants?

11 votes
2 answers
310 views

What is a commuting conversion and why are they problematic?

16 votes
1 answer
1k views

So many data types, so little time

11 votes
2 answers
423 views

Replacing (strict) positivity with monotonicity on propositions

9 votes
2 answers
275 views

What is hereditary substitution and why should I use it?

11 votes
0 answers
153 views

Is there a proof assistant (or an embedding) for the (co)end calculus?

13 votes
2 answers
173 views

Tools for checking the consistency of a type theory

19 votes
2 answers
211 views

What is the difference between judgmental equality, definitional equality, and equality types?

14 votes
1 answer
255 views

Why should you "never resort to polymorphism when initiality would do"?

18 votes
2 answers
359 views

What are the motivations for different variants of categorical models of dependent type?

Browse more Questions