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

8 votes
1 answer
150 views

Type Checking Undecidable in Extensional Type Theory

5 votes
1 answer
97 views

How do I convince the Lean 4 type checker that addition is commutative?

3 votes
1 answer
107 views

What are instances of a dependent pair type?

14 votes
3 answers
452 views

Bringing OOP features into proof assistants?

25 votes
2 answers
3k views

Has anyone ever accidentally "proven" a false theorem with type-in-type?

6 votes
0 answers
108 views

How to write heavily indexed proofs?

18 votes
2 answers
359 views

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

10 votes
1 answer
165 views

Easy ways to introduce inductive types

29 votes
3 answers
827 views

What are the bases for different Proof Assistants?

4 votes
1 answer
89 views

How to elaborate with dependent records present?

15 votes
2 answers
237 views

Are Logics Based on Dependent Types Stronger Than Ones Without?

9 votes
2 answers
197 views

What's the relationship between refinement types and dependent types?

13 votes
2 answers
166 views

What are the upsides and downsides of typed vs untyped conversion?

4 votes
1 answer
105 views

How to implement first-order relational structures in Coq?

Browse more Questions