{"id":"palomar/PALOMAR-2026-10-16-000007","url":"https://github.com/AItoBit/continuum-hypothesis-lean4/tree/c8d3b542530e1b0c9817fad5febd6dfb0298f608","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000007-v1.json","repo":"https://github.com/AItoBit/continuum-hypothesis-lean4","tags":["math.LO","msc:03E50","msc:03E35","msc:03B35","set-theory","continuum-hypothesis","forcing","lean"],"score":0,"title":"Continuum hypothesis independence: a Flypitch reproduction","trust":"high","domain":"math.LO","source":"palomar","authors":["Alexander"],"reviews":0,"subject":"math.LO","summary":"An attributed adaptation of the Flypitch formal proof of two-sided syntactic independence of the continuum hypothesis from its explicitly encoded first-order ZFC theory. Cohen and collapse Boolean-valued models, together with soundness, establish that neither the encoded CH sentence nor its negation is derivable. The development uses an expanded language with definable set operations, collection and Zorn's lemma. It does not supply a formal translation to membership-only ZFC or determine the truth of CH for the ambient Lean reals. This is a reproduction of established work, not a new…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-16","reactions":{},"formalized":true,"formalizes":[{"title":"A Formal Proof of the Independence of the Continuum Hypothesis","identifier":"doi:10.1145/3372885.3373826","relationship":"formalizes"}]}