Explore our questions

1 vote
1 answer
28 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

1 vote
1 answer
30 views

How do I write bitwise logic in lean4 with mathlib?

1 vote
0 answers
63 views

How exactly solved metas "revisited" in an efficient dependent type checker?

1 vote
2 answers
76 views

How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?

2 votes
1 answer
142 views

What is the well-established η law for naturals?

1 vote
1 answer
49 views

What is the official way to reinstall Lean4 from scratch on a Mac or Linux?

2 votes
3 answers
89 views

Induction on indexed type family without JMeq

0 votes
1 answer
44 views

Coq - Overloading over multiple parameters with canonical structures

0 votes
0 answers
18 views

How does one create a lean project even if it already exists e.g., lake +leanprover/lean4:nightly-2023-02-04 new my_project math?

1 vote
1 answer
41 views

Inductively proving that a number is either even or odd in Lean

3 votes
1 answer
90 views

Stuck in a proof about sum types and nonempty lists

3 votes
1 answer
138 views

Recursive notations with forall quantifier

9 votes
2 answers
565 views

What is the state of the art in proof automation in HoTT/CuTT?

6 votes
2 answers
237 views

Lean and inaccessible cardinals

Browse more Questions