Explore our questions

3 votes
0 answers
35 views

Inductive from CoInductive?

0 votes
1 answer
41 views

Lean4 instance management

0 votes
0 answers
84 views

Trouble proving a theorem using induction in Coq

1 vote
1 answer
51 views

How do I enable this kind of rewriting?

4 votes
1 answer
208 views

Dealing an equality with coq. - beginner's question

0 votes
1 answer
54 views

Coq, Merging two forall definitions ranging over the same types

1 vote
1 answer
82 views

Applying universally quantified equalities to propositions

0 votes
1 answer
64 views

Using lean4 to prove subset properties

2 votes
0 answers
42 views

Bounding Volume Proof Assistant Library

11 votes
3 answers
567 views

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

2 votes
1 answer
79 views

How to use a lemma that is defined in a Coq module?

0 votes
1 answer
91 views

How to prove commutation of a recursive function over a finite set encoded with binary nat in coq

1 vote
1 answer
27 views

Lean 4 directive to always include a section variable

0 votes
3 answers
76 views

Why can't Lean4 evaluate my function despite it being defined, Error: compiler IR check failed at '_eval', error: unknown declaration 'g'?

Browse more Questions