Lean 4 vibe-port of Flypitch (continuum hypothesis independence)

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 (which is from…. set theory iirc) 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.