Write a Blog >>
POPL 2020
Sun 19 - Sat 25 January 2020 New Orleans, Louisiana, United States
POPL 2020 (series) / CPP 2020 (series) / The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs /

A Formal Proof of the Independence of the Continuum Hypothesis

Jesse Michael Han, Floris van Doorn
CPP 2020
Tue 21 Jan 2020 17:12 - 17:34 at Maurepas - Formalized mathematics 2 Chair(s): Tobias Nipkow

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 $\sigma$-closed forcing for the consistency of $\mathsf{CH}$.

https://flypitch.github.io/assets/flypitch-cpp.pdf
https://doi.org/10.1145/3372885.3373826
small-avatar
Jesse Michael Han
University of Pittsburgh
small-avatar
Floris van Doorn
University of Pittsburgh
United States

Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

16:50 - 17:56
Formalized mathematics 2CPP at Maurepas
Chair(s): Tobias Nipkow Technische Universität München
16:50
22m
Talk
The Poincaré-Bendixson Theorem in Isabelle/HOL
CPP
Fabian Immler Carnegie Mellon University, Yong Kiam Tan Carnegie Mellon University, USA
DOI Pre-print Media Attached
17:12
22m
Talk
A Formal Proof of the Independence of the Continuum Hypothesis
CPP
Jesse Michael Han University of Pittsburgh, Floris van Doorn University of Pittsburgh
DOI Pre-print Media Attached
17:34
22m
Talk
The Lean mathematical library
CPP
The mathlib Community
DOI Pre-print Media Attached File Attached