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

7 votes
0 answers
95 views

Tutorial implementations of extensional type theories

9 votes
1 answer
141 views

Normalization by evaluation for extensional type theories

7 votes
2 answers
232 views

How do I install Lean 4?

3 votes
1 answer
112 views

Is there a way to use higher order abstract syntax with linear types?

3 votes
0 answers
81 views

Recursive notations with forall quantifier

6 votes
1 answer
200 views

Tracing the classical reasoner in Isabelle

11 votes
1 answer
243 views

auto-generating the proof of infinitude of primes

8 votes
2 answers
261 views

Strong induction on ℕ with function α → ℕ

5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

28 votes
1 answer
269 views

In Lean, what do double curly brackets mean?

2 votes
2 answers
437 views

Lean: dubious noncomputability

2 votes
0 answers
46 views

SSReflect tuple constructor: why not use phantom?

3 votes
0 answers
55 views

Unfolding expressions in Coq by one layer

Browse more Questions