The Flypitch project aimed to produce a formal proof of the independence of the continuum hypothesis.
We have completed our original objective. We are now refining our library and exploring other formalization projects related to forcing and mathematical logic.
Our formalization uses Lean, an open source theorem prover and programming language primarily developed by Leonardo de Moura at Microsoft Research.
The Flypitch project was launched by Jesse Michael Han at the University of Pittsburgh in August 2018. After Floris van Doorn joined the project, work on the current codebase began in October 2018. We have completed a formalization of forcing and the unprovability of the continuum hypothesis in April 2019, and we finished a formal proof of the independence of the continuum hypothesis in September 2019.
To view instructions on downloading, compiling, and viewing the project, see the download page.