We have completed our original objective. We are now refining our library and exploring other formalization projects related to forcing and mathematical logic.
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.