A Formal Proof of the Independence of the Continuum Hypothesis

Abstract

We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \mathsf{CH}$ and a $\sigma$-closed forcing for the consistency of $\mathsf{CH}$.

14 pages, CPP 2020 (pp. 353-366)

Cited by in corpus (4)

• The Lean mathematical library
• Maintaining a Library of Formal Mathematics
• Peano: Learning Formal Mathematical Reasoning
• Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis