The Flypitch project aims to produce a formal proof of the independence of the continuum hypothesis.
A conventional human-readable account of the proof written in type-theoretic foundations, upon which some parts of the formalization will be based, is located here.
To compile the Flypitch project, you will need Lean 3.4.2. Installation instructions for Lean can be found here.
The leanpkg.toml file points to a certain commit of mathlib, which will be cloned into the project directory. 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
To view the project, we recommend the use of a Lean-aware editor like Emacs or VSCode. Among other things, like type information, such editors can display the proof state inside a tactic block, making it easier to understand how theorems are being proved.
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.
Files only depend on files on lines above it
to_mathlib pSet_ordinal bvm fol cohen_poset colimit set_theory abel bfol bv_prf bvm_extras compactness normal realization regular_open_algebra zfc zfc_expanded zfc' cantor_space completion language_extension peano zfc_consistent henkin forcing completeness conservative_extension independence reflection