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 mathlib¹, 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 /src/summary.lean, containing #print statements of important definitions and duplicated proofs of the main theorems. From there, one may use their editor’s jump-to-definition feature to trace the dependencies of the definitions and proofs. A more detailed summary can be found at the project repository.