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

Top 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

39 votes
2 answers
708 views

Are some proof assistants better suited for given areas of math than others?

2 votes
4 answers
195 views

I'm stuck trying to prove ∀x : ℕ, 3 | (x + 5x) with Coq

13 votes
6 answers
951 views

Is there any example of a dependent product that makes sense in a non-type-theory context?

6 votes
1 answer
150 views

What is a neutral term?

3 votes
2 answers
67 views

How to run the main function in lean 4?

3 votes
0 answers
56 views

What are some "real world" first order logical theories for demos?

4 votes
1 answer
85 views

Looking for an entry point in the universe of proof assistants and proof IDE's

12 votes
0 answers
147 views

How do Coq's bidirectionality hints (`&`) affect type checking?

5 votes
1 answer
97 views

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

14 votes
3 answers
719 views

Do you need a Hilbert style Epsilon operator for definitions in set theory?

11 votes
3 answers
587 views

Calculus of (inductive) Constructions: Do inductive definitions increase proof strength?

7 votes
0 answers
62 views

What is focusing and how do I use it?

8 votes
3 answers
511 views

Construction of inductive types "the hard way"

3 votes
0 answers
73 views

How to deal with axioms in a proof assistant?

13 votes
9 answers
408 views

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

6 votes
3 answers
130 views

Preserve equality with match expression

10 votes
1 answer
133 views

Explicit vs implicit universes in lean

3 votes
1 answer
107 views

What are instances of a dependent pair type?

14 votes
1 answer
458 views

What does the "motive is not type correct" error mean in Lean?

6 votes
1 answer
832 views

In Lean, contradiction tactic failed but actually goal accomplished

15 votes
1 answer
96 views

Extends vs including a typeclass argument

4 votes
2 answers
133 views

Turning off some sProp checks

13 votes
3 answers
647 views

How to extract the witness from exists in Coq in function notation/without destructing?

3 votes
1 answer
133 views

Coq defining a hierarchy of collections of integers with infinitely many "levels"

4 votes
0 answers
67 views

Display style proofs using Coq

4 votes
0 answers
49 views

Tactic unification vs evarconv in Coq

4 votes
1 answer
144 views

In (CHM/CCHM) cubical type theory, how to conversion-check face formulae?

10 votes
1 answer
157 views

Is there a Mizar-like sublanguage for Coq?

9 votes
1 answer
531 views

What axioms do I need to search the naturals?

9 votes
1 answer
242 views

Current status of cubical inductive families

6 votes
2 answers
146 views

Policies on introducing free variables when rewriting?

10 votes
1 answer
223 views

How to implement the type checking of `transp` in de Morgan cubical type theory?

8 votes
2 answers
410 views

Curly Braces and Lambdas in Agda

3 votes
3 answers
426 views

How can I prove this theorem with induction in Coq?


Looking for more? Browse the complete list of questions, or popular tags. Help us answer unanswered questions.