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

13 votes
3 answers
647 views

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

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?

8 votes
3 answers
511 views

Construction of inductive types "the hard way"

6 votes
1 answer
832 views

In Lean, contradiction tactic failed but actually goal accomplished

9 votes
1 answer
531 views

What axioms do I need to search the naturals?

2 votes
4 answers
195 views

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

2 votes
2 answers
437 views

Lean: dubious noncomputability

11 votes
1 answer
243 views

auto-generating the proof of infinitude of primes

6 votes
1 answer
200 views

Tracing the classical reasoner in Isabelle

9 votes
1 answer
242 views

Current status of cubical inductive families

4 votes
2 answers
133 views

Turning off some sProp checks

5 votes
2 answers
152 views

How to prove in Lean that sums are distributive?

6 votes
1 answer
150 views

What is a neutral term?

9 votes
1 answer
141 views

Normalization by evaluation for extensional type theories

4 votes
1 answer
144 views

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

3 votes
1 answer
112 views

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

3 votes
2 answers
67 views

How to run the main function in lean 4?

12 votes
0 answers
147 views

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

3 votes
1 answer
107 views

What are instances of a dependent pair type?

5 votes
1 answer
97 views

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

4 votes
1 answer
85 views

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

3 votes
0 answers
81 views

Recursive notations with forall quantifier

7 votes
0 answers
62 views

What is focusing and how do I use it?

3 votes
0 answers
73 views

How to deal with axioms in a proof assistant?

4 votes
0 answers
67 views

Display style proofs using Coq

3 votes
0 answers
56 views

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

3 votes
0 answers
55 views

Unfolding expressions in Coq by one layer

4 votes
0 answers
49 views

Tactic unification vs evarconv in Coq

2 votes
0 answers
46 views

SSReflect tuple constructor: why not use phantom?


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