← All papers
A Formal Proof of the Independence of the Continuum Hypothesis
math.LO
Feb 4, 2021 · v1
TL;DR
Formalizes the independence of the continuum hypothesis using Boolean-valued forcing in Lean.
Abstract
We describe a formal proof of the independence of the continuum hypothesis (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 not-CH and a sigma-closed forcing for the consistency of CH.
Problem
The independence of the continuum hypothesis (CH) from ZFC is a landmark result in set theory, but it had not been formally verified in the Lean theorem prover.
Approach
The authors give a formal proof of the independence of CH in Lean using Boolean-valued models to provide forcing arguments for both directions. Cohen forcing establishes the consistency of not-CH, and a sigma-closed forcing establishes the consistency of CH.
Results
Both directions of the independence of the continuum hypothesis are formally verified in Lean using Boolean-valued models, covering Cohen forcing for not-CH and sigma-closed forcing for CH.