Questions tagged [lean-community]
The GitHub account `leanprover-community` which holds `mathlib`. This should not be confused with the GitHub account `leanprover` which holds the Lean source code.
6 questions
3
votes
1
answer
427
views
What is the official way to reinstall Lean4 from scratch on a Mac or Linux?
I want to install Lean from scratch to see if I can fix a previous issue related to the location where I can create lean projects (and a related issue).
The official instructions don't seem to make it ...
0
votes
0
answers
39
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?
I want to initialize a lean project but the folder I have already exists. How do I do this?
e.g.,
...
1
vote
2
answers
468
views
How does one create a lean project and have mathlib import work when not creating the lean project at the $HOME directory?
I want to create a lean project inside another folder besides the $HOME folder. So I was going through the official Creating a Lean project instructions on how to ...
0
votes
2
answers
202
views
Differential Topology and Differential Geometry Porting to Mathlib4
Simple question, but I started working with Lean after Lean 4 came out, so I'm not familiar with Lean 3. To what extent have the Mathlib3 differential topology and differential geometry libraries been ...
32
votes
1
answer
1k
views
What will happen to mathlib when we transition to Lean 4?
Today, there's an exciting large-scale effort to digitize mathematics in Lean's mathematics library mathlib.
I understand that a transition to Lean 4 is looming. I'...
22
votes
1
answer
442
views
What is the difference between `leanprover` and `leanprover-community` GitHub repositories?
I keep bumping into references to "Lean", but then find there are two GitHub repositories for Lean:
https://github.com/leanprover
and
https://github.com/leanprover-community
Can someone ...