This repository contains the mechanization of the Independence of the Continuum Hypothesis in Isabelle/ZF.

We have reported our mechanization in the article:

``The formal verification of the ctm approach to forcing'', available at https://www.sciencedirect.com/science/article/abs/pii/S0168007224000101

The formal development can be found at the AFP: https://www.isa-afp.org/entries/Independence_CH.html