Skip to main content

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.

Filter by
Sorted by
Tagged with
32 votes
1 answer

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'...
Dustin G. Mixon's user avatar
22 votes
1 answer

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: and Can someone ...
Guy Coder's user avatar
  • 2,846
2 votes
1 answer

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 ...
Charlie Parker's user avatar
1 vote
2 answers

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 ...
Charlie Parker's user avatar
0 votes
2 answers

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 ...
Alex Byard's user avatar
0 votes
0 answers

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., ...
Charlie Parker's user avatar