Formalizing the Independence of the Continuum Hypothesis

Abstract:

Forcing is a technique for constructing new models of set theory where certain statements are "forced" to be true or false, e.g. the axiom of choice, or the continuum hypothesis. We describe a formalization of forcing using Boolean-valued models in the Lean theorem prover. As an application of our framework, we specialize our construction to a Boolean completion of the Cohen poset and formally verify in the resulting model the failure of the continuum hypothesis. Time permitting, we will discuss work in progress on a formal proof of the independence of the continuum hypothesis.

This is joint work with Floris van Doorn.