Skip to content
A formal proof of the independence of the continuum hypothesis
Lean
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
old Bump mathlib, move `conservative_extension.lean` to `/old` May 22, 2019
src Prepare for release May 24, 2019
.gitignore Prepare for release May 24, 2019
LICENSE
README.org Update README Jul 31, 2019
leanpkg.toml Prepare for release May 24, 2019

README.org

Flypitch

Goals

The Flypitch project aims to produce a formal proof of the independence of the continuum hypothesis.

Documentation

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.

Compilation

To compile the Flypitch project, you will need Lean 3.4.2. Installation instructions for Lean can be found here.

The master branch is frozen at the same commit as the latest release. The project is being actively developed on the dev branch.

The leanpkg.toml file points to a certain commit of mathlib, which will be cloned into the project directory. After cloning or extracting 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 and navigating the project

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.

We also have a formula pretty-printer which prints de Bruijn indexed-formulas as their named representations. Code and examples for the pretty-printer can be found in /src/print_formula.lean.

Papers

Our paper A formalization of forcing and the unprovability of the continuum hypothesis, describing this release, was accepted to ITP 2019. It is available here.

Citation information:

@inproceedings{DBLP:conf/itp/2019,
  author    = {Jesse Michael Han and Floris van Doorn},
  title     = {A formalization of forcing and the unprovability of the continuum hypothesis},
  editor    = {John Harrison and John O'Leary and Andrew Tolmach},
  booktitle = {Interactive Theorem Proving - 10th International Conference, {ITP}
               2019, Portland, OR, USA, Sep 9-12, 2019, Proceedings},
  series    = {LIPIcs},
  volume    = {141},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  year      = {2019},
  note      = {To appear}
}

Contributors

You can’t perform that action at this time.