A Formalised Theorem in the Partition Calculus
Lawrence C. Paulson
TL;DR
This paper formalizes a theorem in the partition calculus related to ordinal partitions using Isabelle/HOL, demonstrating the value of formal verification in correcting and understanding complex mathematical proofs.
Contribution
It introduces a formal proof of a theorem in the partition calculus within Isabelle/HOL, including a set theory library, advancing formal verification in mathematics.
Findings
Formal proof highlights corrections in the original theorem
Demonstrates the effectiveness of Isabelle/HOL for complex proofs
Supports future formalization efforts in set theory and combinatorics
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Mathematical Identities · History and Theory of Mathematics · Advanced Algebra and Logic