Return to Question

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.

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.

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.

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.

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.

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.