7

The website Formalizing 100 Theorems by Freek Wiedijk contains a list of some theorems that were chosen at some point as good candidates for formalization (because of their complexity, their importance, etc.) This website seems to be updated very often.

Among the proofs not yet formalized is that of the independence of the Continuum Hypothesis from the axioms of set theory.

What is the current state of the formalization of the independence of $\mathit{CH}$ from $\mathit{ZFC}$?

I browsed this site for more information, and I found this recent question, as well as this one and this, and an answer in math.SE. But I couldn't find information directly concerned with my question.

EDIT. We finished our formalization of the countable transitive model approach to forcing and the independence of $\mathit{CH}$. The paper is available here and at the arXiv.

Martin Sleziak
  • 4,608
Pedro Sánchez Terraf
  • 954
  • 1
    The [proof-theory] tag was suggested on this, but it seems to me that this is a little different: This one is just about implementing some of the usual proofs. But I'll be glad to hear some argument supporting the tag. – Pedro Sánchez Terraf Mar 25 '17 at 11:40
  • 3
    http://math.stackexchange.com/questions/2205154/are-there-any-recent-advances-in-formalizing-the-undecidability-of-mathitch – Asaf Karagila Mar 27 '17 at 13:25
  • 1
    This is great! But what is the exact theorem that you formalized? The countable transitive model approach to forcing, after all, does not achieve the strongest form of the result. Also, why did you choose that approach rather than the Boolean-valued model approach, which seems more direct and also more general and powerful? – Joel David Hamkins Mar 19 '24 at 22:24
  • 1
    Thanks @JoelDavidHamkins! We (only) prove, in ZF, that given a ctm of ZFC, there exist models of ZFC+CH and ZFC+¬CH. We actually identify the always anonymous "sufficient amount of replacement" (though Matthias already knew about this).

    We chose ctms because that's the first approach we understood ;-). We discuss this for the comparison to the Lean formalization. BVM are indeed more elegant.

     – Pedro Sánchez Terraf Mar 19 '24 at 22:36
  • Isn't that version of the theorem provable even in PA or much less? One doesn't need ZF in the background once one has the countable transitive model. – Joel David Hamkins Mar 20 '24 at 01:07
  • Of course! But that is a totally different formalization project. We would have to work essentially from scratch to do that. Here we could reuse some material on relativization already available using ZF.

    Motivated by this, I asked about proof assistants with the ability to work with different metatheories here, but I guess there is not much support on that yet.

     – Pedro Sánchez Terraf Mar 21 '24 at 12:20
  • (There are actually a bit stronger versions which talk about ctms of fragments of ZFC, but anyone interested can check that on the paper.) – Pedro Sánchez Terraf Mar 21 '24 at 12:34

1 Answers1

8

Jesse Michael Han and Floris van Doorn recently formalized the independence of the continuum hypothesis in the Lean theorem prover. See the Flypitch project webpage for their papers and code.

j.c.
  • 13,490
  • 1
    Thanks, I'm aware of their results. Actually, this surprised us in the middle of our development of the ctm approach to forcing in Isabelle/ZF (for instance see here). We'll soon upload some new material on that. – Pedro Sánchez Terraf Jan 02 '20 at 13:12