I ported Flypitch from Lean 3 to Lean 4 over the course of approximately a week, mostly unattended Claude.

The proof of the independence of the continuum hypothesis is a Gödel + Cohen result that deals with the cardinality of the naturals vs. the reals.

That is to say, it states that ZFC (from set theory) cannot prove or disprove the existence of a “size” of infinity between that of the Naturals and that of the Reals. The proof uses a technique called forcing (Cohen) and constructible sets (Gödel).

The Lean 3 version of the proof was written in 2018-2020 by Jesse Han, and Floris van Doorn. It’s one of the significant early Lean proofs.

Lean Zulip thread.

Notes: SFLean meetup

1 June 2026. Elliott presented on my formalization.

  • ZFC is from set theory

  • what is / isn’t possible within mathematical foundations

  • ch: assertion that the cardinality of the reals is the first uncountable infinity? aleph_1

  • comes fine from foundations

  • 1930s: gödel: it’s relatively consistent

  • took an arbitrary universe, restricted it to minimum definable sub-universe: gödel’s L

  • not arbitrary powersets, but a specific set of them

  • L satisfaction ZFC + GCH

  • Use 2 kinds of algebras - “homogeneity”

    • Cohen algebra (forces not CH) for aleph2
    • this is a boolean algebra (algebraic structure like a group or ring where you have a union / intersection)
    • sets with everything in it
    • “truth value”
    • adds a generic real
    • take a topological copy of 2 copies, then we prove it forces w/ value 1, not CH

  • “models” are tricky - kinda pathological - when formalizing, easier to work directly with boolean propositions

  • New language w/ these booleans objects

  • set theory has “compactness” (inherited from first-order logic)

  • Lévy collapse the algebras - forces them to make cardinal countable

segue: where do we do the thing in the flypitch4 port?

  • summary.lean to start
  • Bfol.lean - boolean first order model
  • Bvm.lean
  • (lean isn’t super well suited to set-theory n.b.)
  • PSetOrdinal.lean (presets) - might be able to use the mathlib versions instead?
  • CantorSpace.lean
  • Forcing.lean describes cohen algebra
  • Collapse.lean does the collapse algebra
  • proves the continuum is same aleph1
  • there’s stronger forcing that can add a bijection between the two and made them all countable
  • countable chain condition - need to prove that the aleph2 forcing doesn’t collapse any…. cardinals?
  • zfc, zfc+ch, zfc+notCH are ¿number-theoretically equivalent?
    • adding / denying CH proves no new arithmetic theorems