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}$.

#### Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change

 16:50 - 17:56: Formalized mathematics 2CPP at Maurepas Chair(s): Tobias NipkowTechnische Universität München 16:50 - 17:12Talk The Poincaré-Bendixson Theorem in Isabelle/HOLCPPFabian ImmlerCarnegie Mellon University, Yong Kiam TanCarnegie Mellon University, USA DOI Pre-print Media Attached 17:12 - 17:34Talk A Formal Proof of the Independence of the Continuum HypothesisCPPJesse Michael HanUniversity of Pittsburgh, Floris van DoornUniversity of Pittsburgh DOI Pre-print Media Attached 17:34 - 17:56Talk The Lean mathematical libraryCPP DOI Pre-print Media Attached File Attached