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

10 votes
3 answers
121 views

Given `A = B`, how to prove `a: A` also has type B in Lean 4

3 votes
2 answers
897 views

Using proof assistants to generate fast code

4 votes
2 answers
146 views

Formalization of abstract definitions

6 votes
2 answers
110 views

Why are impredicative constructions used less in type theory than in material set theory?

1 vote
2 answers
233 views

Is it possible to prove (-> (= (Either Trivial Trivial) (left sole) (right sole)) Absurd) in Pie?

5 votes
2 answers
121 views

Unclarity about Preorder class in Lean4

-2 votes
1 answer
181 views

A project in Lean which involves "programming"

6 votes
1 answer
162 views

How to implement a visual proof assistant?

0 votes
2 answers
107 views

Coproducts in Lean

4 votes
1 answer
116 views

Can we completely erase propositions in the type checker?

2 votes
1 answer
103 views

Canonical forms of combinators

2 votes
3 answers
76 views

Equality of records with members whose types are dependent (Lean 4)

5 votes
1 answer
194 views

Very dependent functions

3 votes
1 answer
65 views

Is 'subsingleton elimination' the same concept as 'function comprehension'?

1 vote
2 answers
105 views

Does quantification over functions (STLC) increase strength beyond first order logic?

2 votes
1 answer
80 views

Does there exists a logical format so that my app can export in that format, and the existing popular proof assistants can take it as input?

2 votes
1 answer
92 views

Natural deduction with coq assistant prover

1 vote
2 answers
54 views

Suppressing notation in Lean

4 votes
1 answer
144 views

How important is global choice (a la Lean, HOL Light, Isabelle/HOL) practically?

1 vote
1 answer
111 views

Can I unfold not all things but only one thing in Coq?

3 votes
1 answer
119 views

Equality type and Propositions

1 vote
1 answer
83 views

Why is the normal form of an ind-Nat expression with a function type an elimination-of-a-function expression

1 vote
1 answer
105 views

Does Agda's --injective-type-constructors flag have canonicity?

1 vote
1 answer
79 views

How do I prove this property in Coq?

1 vote
1 answer
76 views

Making a finite graph type in Lean - introduction rule

5 votes
0 answers
89 views

Can we bring unification results under cofibrations outside?

1 vote
1 answer
69 views

Inductive types associated to instances of a structure in Lean

1 vote
1 answer
51 views

Question about default definitions in fields

1 vote
1 answer
49 views

How can I use a (three terms) decidable axiom in a case analysis?

2 votes
1 answer
60 views

Why does an internal term produced by Lean's equation compiler have holes in it?

0 votes
1 answer
40 views

How can I correspond a hypothesis to a decidable axiom in match (in Coq)?

0 votes
0 answers
47 views

If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?

2 votes
1 answer
26 views

How to unfold definitions in Lean / find the right theorems to apply?

3 votes
0 answers
20 views

.CoqMakefile.d required by CoqMakefile but not generated


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