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
1 answer
194 views

Very dependent functions

4 votes
2 answers
146 views

Formalization of abstract definitions

7 votes
1 answer
201 views

Can you build W-types out of natural numbers predicatively?

7 votes
0 answers
177 views

Alternatives to universe levels

5 votes
0 answers
49 views

What are Generic Arguments in Coq and how are they structured in their OCaml code?

9 votes
1 answer
200 views

Type Checking Undecidable in Extensional Type Theory

6 votes
1 answer
158 views

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

4 votes
1 answer
121 views

What are instances of a dependent pair type?

15 votes
3 answers
470 views

Bringing OOP features into proof assistants?

28 votes
2 answers
3k views

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

6 votes
0 answers
113 views

How to write heavily indexed proofs?

18 votes
2 answers
387 views

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

10 votes
1 answer
181 views

Easy ways to introduce inductive types

29 votes
3 answers
931 views

What are the bases for different Proof Assistants?

Browse more Questions