A formalization of forcing and the unprovability of the continuum hypothesis

This repository contains the source code for the paper A formalization of forcing and the unprovability of the continuum hypothesis, which appeared at ITP 2019.

Citation information

@inproceedings{DBLP:conf/itp/HanD19,
  author    = {Jesse Michael Han and
               Floris van Doorn},
  title     = {A Formalization of Forcing and the Unprovability of the Continuum
               Hypothesis},
  booktitle = {10th International Conference on Interactive Theorem Proving, {ITP}
               2019, September 9-12, 2019, Portland, OR, {USA.}},
  pages     = {19:1--19:19},
  year      = {2019},
  crossref  = {DBLP:conf/itp/2019},
  url       = {https://doi.org/10.4230/LIPIcs.ITP.2019.19},
  doi       = {10.4230/LIPIcs.ITP.2019.19},
  timestamp = {Sat, 07 Sep 2019 02:31:13 +0200},
  biburl    = {https://dblp.org/rec/bib/conf/itp/HanD19},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

Viewing the paper

To view the paper, grab the latest release.