Explore our questions

0 votes
1 answer
41 views

Lean4 instance management

3 votes
2 answers
113 views

Lean4: How to construct an HEq between dependent functions?

23 votes
4 answers
490 views

To what extent is formalized mathematics publishable?

1 vote
2 answers
108 views

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

0 votes
1 answer
100 views

Shortcut proof by calculation for addition/subtraction, "The Mechanics of Proof", and mathlib4

6 votes
2 answers
340 views

Type Theory Lean 3 to Lean 4

2 votes
0 answers
136 views

Highschool level linear algebra

2 votes
1 answer
319 views

How to write this non-constructive proof in Lean?

4 votes
2 answers
145 views

How to think about writing Lean theorems

2 votes
1 answer
158 views

Understanding Mathlib/MeasureTheory Notation

0 votes
1 answer
68 views

Automatic nightly Lean update?

4 votes
1 answer
1k views

Lean 4 Importing into VSCode

2 votes
1 answer
81 views

Converting Lean formulations of Lemmas to Coq formulation

32 votes
1 answer
1k views

What will happen to mathlib when we transition to Lean 4?

Browse more Questions