A Formalization of Forcing and the Unprovability of the Continuum Hypothesis.

Jesse Michael Han, Floris van Doorn

Browse the full ITP paper archive.