Machine formalization of infinitary combinatorics proofs (Isabelle/HOL, Lean)

Statement

Machine formalization of infinitary combinatorics is the practice of re-expressing a proof whose objects are *infinite* — ordinals, cardinals, infinite partitions/colourings, generic filters, transfinite inductions — as a term in a proof assistant's kernel (Isabelle/HOL or Lean 4), so that a fixed, small, trusted kernel mechanically certifies every step, including the transfinite-recursion and choice-principle steps that informal papers in this area routinely leave partially implicit. The dominant instance in this wiki's source base is Lawrence Paulson's programme (with Mirna Džamonja and Angeliki Koutsoukou-Argyraki) formalizing ordinal partition calculus in Isabelle/HOL, built on top of Paulson's own ZFC-in-HOL library — a from-scratch embedding of Zermelo–Fraenkel set theory *inside* Isabelle's simple-typed higher-order logic, rather than switching to a separate untyped set-theoretic logic (contrast Isabelle/ZF, used elsewhere for forcing formalizations, below).

The specific mechanism of ZFC-in-HOL (isa-afp.org/entries/ZFC_in_HOL.html, Paulson, Oct 2019): a single HOL type V represents the universe of sets, with elts :: V ⇒ V set mapping each set-as-element to its (HOL-level) set of elements; classes are represented as V set predicates, with a distinguished sub-predicate for "small" classes (those that correspond to an actual ZF set rather than a proper class); two type classes, embeddable (types that can be injected into V) and small (types whose image under that embedding is always a ZF set), let ordinary HOL types (naturals, pairs, functions) be silently treated as ZF sets wherever needed, "minimising the amount of new notation." Ordinals, cardinals, transfinite induction/recursion, and transitive closure are all built as HOL-level definitions and lemmas *about* V, not as a new logic — so the entire existing Isabelle/HOL proof infrastructure (simp sets, automation, type-class inference) applies uniformly to infinitary set-theoretic reasoning.

The theorems formalized (isa-afp.org/entries/Ordinal_Partitions.html; arxiv.org/abs/2011.13218): using arrow notation $\alpha\to(\beta,m)^2$ (defined in Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program), - Specker's theorem: $\omega^2\to(\omega^2,m)^2$ for every finite $m$; - the Erdős–Milner theorem: $\omega^{1+\alpha\cdot n}\to(\omega^{1+\alpha},2^n)^2$; - Larson's proof of E.C. Milner's unpublished result: $\omega^\omega\to(\omega^\omega,m)^2$ for every $m\in\mathbb N$ (via Nash-Williams's combinatorial-forcing machinery, itself formalized as a separate, reusable AFP entry).

Facts

- AFP entry `Ordinal_Partitions` (Paulson, Aug 3, 2020, isa-afp.org/entries/Ordinal_Partitions.html, BSD license): four Isabelle sessions — Library_Additions, Partitions, Erdos_Milner, Omega_Omega — formalizing Specker's $\omega^2\to(\omega^2,m)^2$, the Erdős–Milner step-up theorem, and Larson's proof of Milner's $\omega^\omega\to(\omega^\omega,m)^2$. Its stated dependencies are the separate Nash_Williams AFP entry and ZFC_in_HOL. - AFP entry `Nash_Williams` (Paulson, May 16, 2020, isa-afp.org/entries/Nash_Williams.html): formalizes Nash-Williams's 1965 generalization of Ramsey's theorem from infinite sets of *fixed-size* subsets to infinite families of *finite sets/lists subject to a "no initial segment" condition*, drawing on Todorčević's *Ramsey Spaces* monograph. This is exactly the "combinatorial forcing" engine listed as technique #4 in Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program — formalized once, independently, then imported as a black box by the harder $\omega^\omega$ proof, mirroring how the informal literature itself layers Nash-Williams underneath Larson's argument. - Overview paper: Džamonja, Koutsoukou-Argyraki & Paulson, "Formalising Ordinal Partition Relations Using Isabelle/HOL," arXiv:2011.13218, published *Experimental Mathematics* 31:2 (2022) 383–400 (Special Issue on Interactive Theorem Proving in Mathematics Research) — a reflective companion paper (not itself new Isabelle code) explaining the design choices and "some of the most challenging aspects of the formalisation process" of the AFP entries above. - Formalization caught a published error: Paulson, "A Formalised Theorem in the Partition Calculus," arXiv:2104.11613 — frames the Erdős–Milner formalization explicitly around the fact that the *original 1972 Erdős–Milner paper itself required a later published correction*; the paper is presented as a demonstration that "formal verification can reveal errors in classical mathematical work" of exactly this transfinite-induction-heavy kind, where an off-by-one in an ordinal-exponent step-up is easy for human referees to miss but impossible for the Isabelle kernel to silently accept. (This matches, independently, the Xena-blog failure-mode catalogue described in Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) for the Lean/finite-combinatorics side — formalization surfacing edge cases informal proofs elide is a *recurring*, cross-system phenomenon, not specific to one proof assistant.) - Isabelle/ZF is a separate, older lineage for infinitary set theory, used specifically for forcing: Gunther, Pagano & Sánchez Terraf, "First steps towards a formalization of Forcing," arXiv:1807.05174, formalize Cohen forcing notions (preorders with top, dense sets, generic filters), the Rasiowa–Sikorski lemma, and generic extensions $M[G]$ — but in Isabelle/ZF, Isabelle's classical first-order ZF-set-theory object logic, *not* the HOL-typed V-embedding used by the ordinal-partition work. This is a live methodological fork within Isabelle itself: ZFC-in-HOL (Paulson) keeps everything inside one strongly-automated typed logic at the cost of building the ZF embedding from scratch; Isabelle/ZF gives a more direct, textbook-faithful rendering of set-theoretic forcing at the cost of a separately-automated, untyped object logic. - The Lean side of the same problem: Lean's mathlib carries its own from-scratch SetTheory.Ordinal/SetTheory.Cardinal library (Mathlib.SetTheory.Cardinal.Ordinal, Mathlib.SetTheory.Cardinal.Arithmetic) built by Mario Carneiro, providing aleph, beth, and infinite-cardinal arithmetic ($\kappa\cdot\kappa=\kappa$) natively as Lean type-theoretic objects rather than via a ZF-in-type-theory embedding — a different foundational strategy from Paulson's V-in-HOL approach (secondary-source claim, not independently confirmed in this session, that part of this library's original motivation was proving the existence of infinitely many inaccessible cardinals in Lean). - Forcing and independence results have also been done in Lean: Han & van Doorn, arXiv:1904.10570, formalize Boolean-valued models and the fundamental theorem of forcing in Lean 3, specializing to the regular-open algebra of Cantor space to give a fully machine-checked proof that CH *fails* in that generic extension — the Lean-side counterpart to the Isabelle/ZF forcing programme above, using a different technique (Boolean-valued semantics rather than Isabelle/ZF's generic-filter/dense-set style). - A further, more recent Lean 4 infinitary-combinatorics/descriptive-set-theory formalization: Manthe, "A formalization of Borel determinacy in Lean," arXiv:2502.03432 (accepted *Annals of Formalized Mathematics* vol. 2, March 2026) — formalizes Gale–Stewart games and Martin's theorem that Borel games are determined, following Martin's purely-inductive proof strategy; evidence that infinitary/descriptive-set-theoretic formalization is an active, ongoing target on the Lean side as well as Isabelle's, not a one-off. - No Lean formalization of the specific ordinal-partition-calculus chain (Specker/Chang/Erdős–Milner/Larson) was found in this session — per Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program's own independently-verified Facts, only an unproved Lean *statement* scaffold exists for the flagship open case (Erdős #592 — characterize the countable partition ordinals) in google-deepmind/formal-conjectures; the *proved* chain up through $\omega^\omega\to(\omega^\omega,m)^2$ exists only in Isabelle/HOL (AFP Ordinal_Partitions) as of this writing.

Technique

When it applies: any completed (not open) infinitary-combinatorics or set-theoretic theorem whose statement quantifies over ordinals, cardinals, or infinite structures and whose proof uses transfinite induction/recursion, well-ordering, combinatorial forcing (Nash-Williams/Galvin–Prikry style, distinct from Cohen forcing), or set-theoretic forcing/generic-extension arguments proper. Two sub-regimes recur, matching the AFP-vs-Isabelle/ZF fork documented above: 1. ZFC-in-HOL-style formalization (Paulson's approach) is the right tool when the target theorem's *combinatorial content* is what matters (ordinal arithmetic, partition relations, Ramsey-type arguments) and one wants full access to Isabelle's HOL-level automation (simp, type classes, auto/blast) throughout — the ZF layer is a thin, largely-invisible embedding, not the star of the proof. 2. Isabelle/ZF or a dedicated set-theoretic object logic is preferable when the proof's content is *itself about models of set theory* — generic extensions, forcing posets, independence results — where staying inside a genuinely untyped, extensional ZF-style universe more directly mirrors the textbook argument (Gunther–Pagano–Sánchez Terraf's choice) than would an embedding trick. 3. On the Lean side, mathlib's native type-theoretic ordinal/cardinal library plays the role of ZFC-in-HOL (infinitary combinatorics reasoning without leaving the ambient type theory), while Boolean-valued models (Han–van Doorn) play the role Isabelle/ZF-style forcing plays for independence results.

Why it works (the mechanism): - Transfinite recursion/induction becomes a checked fixed-point/well-founded-recursion definition, not an informal "and so on by induction on ordinals" gesture. In ZFC-in-HOL, this is literally HOL recursion over the well-founded membership relation on V; the kernel enforces termination and totality exactly where an informal proof might silently assume a limit-ordinal case works "by the same argument," which is precisely the class of step (limit-ordinal case, ordinal-exponent step-up) where the Erdős–Milner 1972 correction originated (arXiv:2104.11613). - Layered reuse mirrors the informal proof's own dependency structure: Nash-Williams's combinatorial-forcing theorem is proved once (AFP Nash_Williams) and then *imported as a lemma* by the harder $\omega^\omega\to(\omega^\omega,m)^2$ proof (AFP Ordinal_Partitions), exactly matching how the informal literature (Larson's proof, per Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program's Technique §4) treats Nash-Williams's theorem as a black-box combinatorial engine rather than re-deriving it. This is the general recipe for scaling infinitary formalization: formalize the *reusable combinatorial lemma* as its own self-contained entry first, so later, harder theorems in the same family can cite it the way a paper cites a previous paper, instead of re-embedding the whole argument. - The type-class/embedding machinery (`embeddable`, `small`) is what lets "ordinary" HOL objects (naturals, finite sequences, functions between them) be silently treated as ZF sets wherever a partition-calculus proof needs to talk about, e.g., a colouring $\chi:[\alpha]^2\to 2$ as a genuine set-theoretic function on a genuine set-theoretic ordinal, without hand-rolling a fresh set-vs-type coercion at every lemma — this is the specific engineering choice that makes ZFC-in-HOL tractable at AFP scale (four linked sessions) rather than a one-off stunt. - Kernel-level certification is what makes "the formalization caught an error the informal literature missed" possible at all: because the kernel accepts *no* implicit ordinal-arithmetic step, an off-by-one or missed limit-case in a step-up induction (exactly the kind of error the original 1972 Erdős–Milner paper needed a correction for) cannot be papered over — it manifests as a sorry, a type error, or an unprovable goal, forcing explicit resolution.

How to actually use it (recipe, as instantiated by the Paulson/Džamonja/Koutsoukou-Argyraki programme): 1. Identify a completed (already-published, ideally already-corrected) infinitary-combinatorics theorem chain with a clear internal dependency structure (base Ramsey-type lemma → intermediate combinatorial-forcing theorem → final step-up/induction result) — ordinal partition calculus is the paradigm case because Specker → Erdős–Milner → Nash-Williams → Larson/Milner is exactly such a chain. 2. Choose the foundational layer: build/reuse a V-in-HOL-style embedding (ZFC-in-HOL) if the target reasoning is combinatorial-over-sets, or use a native untyped set-theoretic object logic (Isabelle/ZF) if the target reasoning is *about* models/forcing/independence. 3. Formalize the reusable combinatorial engine (e.g., Nash-Williams) as its own self-contained library entry *before* attempting the theorem that depends on it, so it can be cited rather than re-proved. 4. Formalize the step-up/induction theorems (Erdős–Milner-style) with special attention to every limit-ordinal and boundary case; expect this to be exactly where the informal proof's implicit gaps (and, per arXiv:2104.11613, its actual historical errors) surface as unprovable Isabelle goals. 5. Publish both the machine artifact (AFP entry, permanent and re-checked on every AFP release) and a reflective paper (arXiv:2011.13218-style) documenting design choices and difficulties, since the *engineering decisions* (which embedding, which type classes) are themselves reusable knowledge for the next infinitary-formalization project, independent of the specific theorem proved.

Related

- Ordinal partition calculus — arrow notation $\\alpha\\to(\\alpha,m)^2$ and the self-partitioning-ordinal program — the mathematical content being formalized: arrow notation, the Specker/Chang/Erdős–Milner/Nash-Williams/Larson theorem chain, and the informal proof techniques (ramification, elementary submodels, interaction schemes, combinatorial forcing, CNF induction) that the Isabelle formalization mirrors step-for-step. - Lean 4 formalization of constructions and conditional reductions (Erdős-problem context) — this wiki's companion page on Lean 4 formalization of *finite/algebraic* Erdős-problem constructions and conditional reductions (Singer's Sidon construction, erdos/30); together the two pages cover the finite-vs-infinitary split in current Erdős-adjacent formalization activity, and share the "formalization surfaces informal gaps/errors" mechanism independently confirmed on both sides (Xena-blog bug catalogue vs. the Erdős–Milner 1972 correction). - Erdős #592 — characterize the countable partition ordinals — the flagship *open* ordinal-partition-calculus question (Schipperus's $\le2$-vs-$\ge4$-summand dichotomy, exactly-3-summands case open); has only an unproved Lean statement scaffold in google-deepmind/formal-conjectures, making it the natural next target for either extending the Isabelle proof chain or porting it to Lean. - Erdős #590 — ω^ω → (ω^ω, 3)² (Chang's ordinal partition theorem) — the $\beta=\omega$ resolved instance (Chang's theorem), the case whose full underlying proof chain (Specker → Erdős–Milner → Nash-Williams → Milner/Larson) is exactly what AFP Ordinal_Partitions + Nash_Williams formalize. - Erdős #591 — is $\omega^{\omega^2}\to(\omega^{\omega^2},3)^2$? — the $\beta=\omega^2$ resolved instance (Specker's theorem), directly one of the two headline results in AFP Ordinal_Partitions.