A formal proof of the independence of the continuum hypothesis
summary
A complete formal proof that the Continuum Hypothesis is independent of ZFC is carried out in Lean 3: 20,000 lines and about a year of work produce a modular deep embedding of first‑order logic, ZFC axioms, and boolean‑valued forcing via inductive B‑names (generalizing pset), with specific boolean algebras (regular open algebra for ¬CH and a function‑space algebra to force CH). Custom automation and tactics handle tedious boolean calculations, the constructions check as models of ZFC, and both independence directions are verified.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 0:53How I heard about this problem
- 1:22The exnihilo argument
- 1:52Formalization
- 2:19What do we need
- 3:29Syntax
- 5:15Function Symbols
- 6:02Forces
- 7:03Set theory
- 8:21Booleanvalued models
- 8:50Do we have to internalize the arguments
- 9:14Key observation
- 9:43Axial
- 11:10Equality
- 11:50Highlevel view
- 14:04Algebra
- 14:55Automation
- 16:42Summary
- 17:48Questions
related talks
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
49mFrom ZX to first order logic: a survey of string diagrammatic calculi
32mSatisfiability Modulo Custom Theories in Z3 (Tool Paper)
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
51mA Gentle Introduction to Modern Model Theory
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
31mA Coq Library of Undecidable Problems
17mA Formally Verified Foundation for Compositional Heterogeneous Coherence