A formalization of forcing and the consistency of the failure 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 3 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. This is joint work with Floris van Doorn.