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.

翻译：我们讨论了计算机验证构造的一些亮点：给定一个可数传递集合模型$M$（满足$\mathit{ZFC}$），构造满足$\mathit{ZFC}+\neg\mathit{CH}$和$\mathit{ZFC}+\mathit{CH}$的力迫扩张。此外，令$\mathcal{R}$为替换公理模式的实例集。我们分离出一个21元素子集$\Omega\subseteq\mathcal{R}$，并定义了$\mathcal{F}:\mathcal{R}\to\mathcal{R}$，使得对任意$\Phi\subseteq\mathcal{R}$和$M$-力迫泛型$G$，若$M\models \mathit{ZC} \cup \mathcal{F}\text{``}\Phi \cup \Omega$，则$M[G]\models \mathit{ZC} \cup \Phi \cup \{ \neg \mathit{CH} \}$，其中$\mathit{ZC}$是带有选择公理的策梅洛集合论。为实现这一目标，我们使用了证明助理Isabelle，并基于L. Paulson等人开发的Isabelle/ZF库开展工作。