Flypitch Lean 4 is an in-progress Lean 4 port of the original Flypitch development.

The eventual target theorem is independence_of_CH. The repository is currently focused on porting the logic-side infrastructure first (syntax, semantics, proof theory, compactness, completion, and language extension machinery) before finishing the forcing and ZFC branch.

Useful links:

• Blueprint
• Blueprint as pdf
• Dependency graph
• Doc pages for this repository
• GitHub repository