A Formal Proof of the Independence of the Continuum Hypothesis

TL;DR

This paper presents a formal proof of the independence of the continuum hypothesis using the Lean theorem prover, employing Boolean-valued models and forcing techniques for both CH and its negation.

Contribution

It is the first formal proof of CH independence in a proof assistant, utilizing Boolean-valued models and forcing within Lean.

Findings

Formal proof of CH independence in Lean

Implementation of Cohen forcing and σ-closed forcing

Verification of consistency results for CH and its negation

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}$.