arXiv:2102.02901math.LO
A Formal Proof of the Independence of the Continuum Hypothesis
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
Abstract
We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \mathsf{CH}$ and a $σ$-closed forcing for the consistency of $\mathsf{CH}$.
> Are these two meanings of "undecidable" related I can't claim to answer this, but you might like to look at A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory[0] which (amongst other interesting things) does discuss the proposition "ZFC is…
ttctciyfView on HNParent context