Download and installation
To download the Flypitch project, use any of the releases listed at the project repository. To compile the Flypitch project, you will need Lean 3.4.2. Installation instructions for Lean can be found here.
Building the project
After cloning the repository to
flypitch, navigate to
flypitch and run
leanpkg configure leanpkg build
This will additionally compile the requisite parts of
mathlib1, and will take multiple minutes.
Optionally, you can install the
update-mathlib script (see here for instructions) which will download pre-built
.olean files, considerably speeding up the compilation. In this case, you can instead run
leanpkg configure update-mathlib leanpkg build
Viewing the project
To view the project, we recommend the use of a Lean-aware editor like Emacs or VSCode. Among other things, like typing information, such editors can display the proof state inside a tactic block, making it easier to understand how theorems are being proved.
Navigating the project
A summary of the main results can be found in
mathlibis Lean’s community-maintained mathematical components library ↩