  We discuss some highlights of our computer-verified proof of the
construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of
generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and
$\mathit{ZFC}+\mathit{CH}$. Moreover, let $\mathcal{R}$ be the set of instances
of the Axiom of Replacement. We isolated a 21-element subset
$\Omega\subseteq\mathcal{R}$ and defined
$\mathcal{F}:\mathcal{R}\to\mathcal{R}$ such that for every
$\Phi\subseteq\mathcal{R}$ and $M$-generic $G$, $M\models \mathit{ZC} \cup
\mathcal{F}\text{``}\Phi \cup \Omega$ implies $M[G]\models \mathit{ZC} \cup
\Phi \cup \{ \neg \mathit{CH} \}$, where $\mathit{ZC}$ is Zermelo set theory
with Choice.
  To achieve this, we worked in the proof assistant Isabelle, basing our
development on the Isabelle/ZF library by L. Paulson and others.

Logic;Logic in Computer Science