{
  "id": "2104.11613",
  "version": "v1",
  "published": "2021-04-23T14:01:09.000Z",
  "updated": "2021-04-23T14:01:09.000Z",
  "title": "A Formalised Theorem in the Partition Calculus",
  "authors": [
    "Lawrence C. Paulson"
  ],
  "categories": [
    "math.LO"
  ],
  "abstract": "A paper on ordinal partitions by Erd\\H{o}s and Milner (1972) has been formalised using the proof assistant Isabelle/HOL, augmented with a library for Zermelo-Fraenkel set theory. The work is part of a project on formalising the partition calculus. The chosen material is particularly appropriate in view of the substantial corrections later published by its authors, illustrating the potential value of formal verification.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2021-04-23T14:01:09.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03E02",
      "03E05",
      "03E10",
      "03B35",
      "68V20",
      "68V35"
    ],
    "keywords": [
      "partition calculus",
      "formalised theorem",
      "proof assistant isabelle/hol",
      "zermelo-fraenkel set theory",
      "ordinal partitions"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}