A formalization of Borel determinacy in Lean

TL;DR

This work formalizes Borel determinacy within Lean 4 by modeling Gale-Stewart games and proving Martin's theorem for Borel payoff sets through a purely inductive approach. Key innovations include the introduction of universal unravelability, a category-theoretic inverse-limit treatment for countable unions, and careful management of partial functions via Lean-specific design choices (junk values vs propositional hypotheses). The formalization demonstrates Lean's capacity to capture intricate descriptive set-theoretic proofs and outlines practical considerations for tactics, automation, and dependent-types in large formalizations. The results suggest that formalizing determinacy for broader classes under large cardinal assumptions is feasible within a proof assistant, with potential benefits for building a descriptive set theory library in formalized mathematics.

Abstract

We present a formalization of Borel determinacy in the Lean 4 theorem prover. The formalization includes a definition of Gale-Stewart games and a proof of Martin's theorem stating that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy".

Theorems & Definitions (5)

• theorem 2.1
• lemma 2.2
• lemma 2.3
• proof : Proof sketch of \ref{['unravsig']}
• proof : Proof sketch of \ref{['unravclo']}