The formal verification of the ctm approach to forcing

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf +1

We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $ZFC$, of generic extensions satisfying $\math…