Skip to main content

Explore our questions

1 vote
1 answer
79 views

Transplanting rocq library files from one computer to another

1 vote
1 answer
138 views

Isar-style proofs for Rocq or Lean?

2 votes
1 answer
184 views

About the use of command Canonical in Coq for mantaining Record Type information

0 votes
0 answers
112 views

Create an olog for Wikipedia policy

11 votes
3 answers
4k views

How do I install Lean 4?

1 vote
1 answer
107 views

Using Lean 4 to formalize Boolean functions and transformations to a DAG

0 votes
1 answer
85 views

How can I proof that a type is non inhabited in lean

1 vote
1 answer
96 views

How to do induction on an expression in Lean 4?

3 votes
1 answer
122 views

In Rocq, can I unfold a single "let _ := _ in _" at a time?

12 votes
0 answers
299 views

Rules for mutual inductive/coinductive types

10 votes
2 answers
1k views

Why does Lean4 use intensional Type Theory when its definitional equality is undecidable anyways?

-1 votes
1 answer
57 views

Install Lean-4 stable on MacBook and use it via emacs

0 votes
1 answer
61 views

Proof that the volume of my cube is greater than zero

1 vote
5 answers
499 views

Formalizing "finite or infinite" in Coq

Browse more Questions