3

I'm cross-posting this from Mathoverflow. Since I'm asking for recent developments, it seems best to have answers in both sites.

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 Mathoverflow for more information, and I found this recent question, as well as this one and this, and an answer in this site. But I couldn't find information directly concerned with my question.

Pedro Sánchez Terraf
  • 4,664
  • 1
    How about the question of mine? There are no answer but Andrej comments on it. – Hanul Jeon Mar 27 '17 at 12:14
  • 3
    MathOverflow: http://mathoverflow.net/questions/265435/are-there-any-recent-advances-in-formalizing-the-undecidability-of-mathitch – Asaf Karagila Mar 27 '17 at 13:25
  • @AsafKaragila Thanks, I forgot to add the link. – Pedro Sánchez Terraf Mar 27 '17 at 16:08
  • @HanulJeon Thank you very much, I'll check the reference you cite in your question. And I'm happy to learn that Andrej's opinions there are essentially what I thought. – Pedro Sánchez Terraf Mar 27 '17 at 16:09
  • Your description of Freek Wiedijk's list is incorrect. Read Freek's commentary right at the top of your link: the list is the result of a light-hearted attempt to make a mathematical contribution to the late 20th century trend for coming up with lists of the top 100 movies, books etc. If anything, the list is rather arbitrary and is a good set of challenge problems because the theorems have not been chosen as good candidates for formalisation. ... – Rob Arthan Mar 27 '17 at 19:51
  • ... You will get better information on the state of the art on formalising the independence of CH if you ask on the mailing lists for the main interactive theorem-proving systems: Coq, HOL and Isabelle. – Rob Arthan Mar 27 '17 at 20:01
  • @RobArthan Thanks for your feedback. In any case, the list does highlight the most difficult problems, and I think it's a nice source (especially, considering how frequently is updated). I'll take your piece of advice, but I think it was worth the try asking here and in MO. In particular, some users are involved in this kind of business, like Mario Carneiro. – Pedro Sánchez Terraf Mar 27 '17 at 23:49
  • 1
    @PedroSánchezTerraf: Freek's list is not intended to highlight the most difficult problems. You are, however, right that it is a nice source of information and that Freek keeps it up to date. And you are right that some MSE users are involved in "this kind of business": in fact, I can think of at least 2. Can you? $\ddot{\smile}$ – Rob Arthan Mar 28 '17 at 20:00
  • 1
    I think your edit should be an answer. – Z. A. K. Mar 19 '24 at 23:36

1 Answers1

1

As per Zoltan Kocsis' suggestion, I'm answering the question with an updated on our developments (formerly, this was an edit to the OP).

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.

The answer to the MO question linked above contains the info about the first formalization of the independence, by Han and van Doorn.

Pedro Sánchez Terraf
  • 4,664