← All papers
A formalization of Borel determinacy in Lean
math.LO
Feb 5, 2025 · v1
TL;DR
Formalizes Borel determinacy in the Lean 4 theorem prover, including Gale-Stewart games and Martin's theorem.
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".
Problem
Borel determinacy (Martin's theorem that all Borel games are determined) is a central result in descriptive set theory provable in ZFC, but it had not been formalized in Lean.
Approach
The authors formalize Borel determinacy in Lean 4, following Martin's purely inductive proof. The formalization includes a definition of Gale-Stewart games, closed determinacy as an intermediate result, and the full inductive proof using auxiliary lifted games and unraveling constructions.
Results
A complete formalization of Borel determinacy is produced in Lean 4. The formalization closely follows Martin's inductive proof, requiring expansions only where the original argument is inherently informal. Design choices around dependent types and partial functions are discussed.