A Formalization of Borel Determinacy in Lean

Basic Information

• Paper ID: 2502.03432
• Title: A formalization of Borel determinacy in Lean
• Author: Sven Manthe
• Classification: math.LO (Mathematical Logic)
• Publication Date: February 2025 (arXiv preprint)
• Paper Link: https://arxiv.org/abs/2502.03432

Abstract

This paper formalizes the Borel determinacy theorem in the Lean 4 theorem prover. The formalization includes the definition of Gale-Stewart games and a proof of Martin's theorem, which establishes that Borel games are determined. The proof closely follows Martin's "A purely inductive proof of Borel determinacy."

Research Background and Motivation

Problem Context

1. Importance of Determinacy Theory: The determinacy of infinite two-player games is a central topic in descriptive set theory, introduced by Gale and Stewart in 1953
2. Theoretical Foundation: While determinacy for large classes of sets is closely related to large cardinals, Borel determinacy can be proven in ZFC set theory
3. Formalization Challenge: Borel determinacy is known for requiring a larger fragment of ZFC than most common theorems, making its formalization particularly challenging

Research Motivation

1. First Formalization: Determinacy beyond closed sets has never been formalized in a proof assistant before
2. Theoretical Verification: To verify that Lean 4's type theory is sufficient to handle theorems requiring strong set-theoretic fragments
3. Technical Exploration: To explore the use of propositional assumptions rather than "junk values" in formalization

Core Contributions

1. First Complete Formalization: The first formalization in a theorem prover of a determinacy result beyond closed sets
2. Technical Innovations:
   • Introduction of the "universal unravelability" concept to replace Martin's transverse induction
   • Use of categorical methods for handling inverse limit constructions
   • Development of automated tactics for handling k-fixing maps
3. Design Choice Verification: Demonstration of the feasibility of using propositional assumptions rather than "junk values" for implementing partial functions
4. Code Scale: Approximately 5000 lines of complete implementation, with foundational definitions comprising less than half

Methodology Details

Core Concept Definitions

Gale-Stewart Games

• Game Structure: G = (T, P), where T is a non-empty pruned tree and P ⊆ T is the payoff set
• Game Rules: Two players (0 and 1) alternately select elements such that the resulting finite sequences lie in T
• Winning Condition: Player 0 wins if the infinite game a ∈ P; otherwise, player 1 wins

Strategies and Determinacy

• Strategy Definition: A strategy σ is a function mapping each position x of player i to a successor position
• Winning Strategy: σ is a winning strategy if all games consistent with σ are won by player i
• Determinacy: A game is determined if at least one player has a winning strategy

Technical Innovations

1. Universal Unravelability Concept

-- Unravelability definition
def Unravelable (T : Tree A) (P : Set [T]) : Prop :=
  ∀ k : ℕ, ∃ (π : T' → T) (φ : Strategy T' → Strategy T), 
    IsKCovering k π φ ∧ IsClopen ([π]⁻¹(P))

-- Universal unravelability (innovation in this paper)
def UniversallyUnravelable (T : Tree A) (P : Set [T]) : Prop :=
  ∀ (π : T' → T) (φ : Strategy T' → Strategy T), 
    IsCovering π φ → Unravelable T' ([π]⁻¹(P))

2. Categorical Framework

Define category C with objects (A,T) pairs (T is a tree on A) and morphisms as length-preserving equivariant maps:

• Limit Construction: Prove that C has all limits
• Functor Properties: Extend the body map T ↦ T to a functor from C to topological spaces
• k-Covering: Covering maps that are bijective on the first k levels

3. Key Lemma Structure

Lemma 3.2 (σ-Algebra Property):

lemma universally_unravelable_sigma_algebra (T : Tree A) :
  IsSigmaAlgebra {P | UniversallyUnravelable T P}

Lemma 3.3 (Universal Unravelability of Closed Games):

lemma closed_games_universally_unravelable (T : Tree A) (P : Set [T]) 
  (h : IsClosed P) : UniversallyUnravelable T P

Proof Strategy

Unraveling Construction for Closed Games

In the unraveled game G':

1. First Move: Player 0 not only selects move a₀ but also chooses their own quasi-strategy σ
2. Second Move: Player 1 either selects a finite sequence x compatible with σ (where she wins all games extending x), or selects a quasi-strategy guaranteeing failure against σ
3. Subsequent Moves: Players proceed according to their chosen strategies

Handling Countable Unions

Using inverse limit construction:

... → T₃ → T₂ → T₁ → T₀

where each transition map is a (k+i)-covering, and the projections of the limit extend to (k+i)-coverings.

Experimental Setup

Implementation Environment

• Theorem Prover: Lean 4
• Mathematical Library: mathlib
• Code Scale: Approximately 5000 lines
• Project Structure: Foundational definitions (<50%) + Formalization of Martin's proof (>50%)

Technical Challenges and Solutions

1. Automated Tactics

Developed automation for handling two classes of assumptions:

• Position Assumptions: "x is a position of player i," reduced to Presburger arithmetic
• k-Fixing Assumptions: Automatic inference of appropriate k values using type class resolution

class Fixing (k : outParam ℕ) (f : S → T) : Prop where 
  prop : IsIso ((res k).map f)

2. Dependent Type Handling

Created an abstract metaprogram to eagerly abstract proof terms into lemmas:

elab "abstract" tacs:ppDedent(tacticSeq) : tactic => do
  let target ← getMainTarget
  let goal ← getMainGoal
  let newGoal ← mkFreshExprMVar target
  setGoals [newGoal.mvarId!]
  Elab.Tactic.evalTactic tacs
  setGoals [goal]
  goal.assign (← mkAuxTheorem ((← getDeclName?).get! ++ 'abstract ++ (← mkFreshId)) target newGoal)

Experimental Results

Formalization Completeness

1. Completeness Verification: Successfully formalized the complete proof of Martin's theorem
2. Type Checking: All definitions and theorems pass Lean 4's type checking
3. Compilability: The entire project compiles and verifies successfully

Comparison with Original Proof

1. Structure Preservation: The proof structure closely follows Martin's original proof
2. Technical Adaptation: Successfully adapted set-theoretic proofs to the type-theoretic framework
3. Innovative Improvements: Avoided transverse induction through the universal unravelability concept

Performance Analysis

1. Compilation Time: Reasonable compilation time (specific values not provided in the paper)
2. Memory Usage: Avoided exponential runtime growth through eager abstraction
3. Automation Effectiveness: Developed tactics significantly reduced manual proof work

Related Work

Game Theory Formalization

1. Joosten (2021): Formalized determinacy of closed games in Isabelle
   • Used coinductive lists to handle both finite and infinite games simultaneously
   • This paper focuses on infinite games, describing partial games only with finite sequences
2. Mathlib: Contains formalization of finite games (SetTheory.Game), following Conway's approach
   • Handles only finite games
   • Determinacy is always satisfied in this context

Descriptive Set Theory

1. Foundational Results: mathlib already includes foundational results in descriptive set theory
2. Missing Content: Several corollaries of Borel determinacy remain formalized
3. Potential Applications: This work can serve as a tool for building a more comprehensive formalized library of descriptive set theory

Conclusions and Discussion

Main Conclusions

1. Feasibility Proof: Demonstrates that formalizing theorems requiring strong ZFC fragments in Lean 4 is feasible
2. Method Effectiveness: Martin's purely inductive method successfully adapts to the type-theoretic framework
3. Technical Innovation: The universal unravelability concept and categorical methods effectively simplify the formalization process

Limitations

1. Theoretical Strength Constraints: Stronger forms of determinacy (such as analytic determinacy) cannot be proven without additional axioms
2. Complexity: The proof-theoretic strength of the proof is reflected in the rapid growth of set cardinalities
3. Domain-Specific: The method is primarily applicable to determinacy problems in descriptive set theory

Future Directions

1. Extended Determinacy: Formalize determinacy for larger classes of sets under large cardinal assumptions
2. Reverse Results: Formalize reverse statements constructing inner models of large cardinals from determinacy
3. Library Enhancement: Utilize Borel determinacy to build a more comprehensive formalized library of descriptive set theory

In-Depth Evaluation

Strengths

1. Pioneering Work: First formalization of determinacy beyond closed sets, marking an important milestone
2. Technical Depth:
   • Clever adaptation of set-theoretic proofs to type theory
   • Innovative introduction of the universal unravelability concept
   • Effective use of category theory to simplify complex constructions
3. Engineering Quality:
   • 5000 lines of high-quality code
   • Comprehensive automation support
   • Good performance optimization
4. Methodological Contribution: Provides valuable insights for handling partial functions in dependent types

Weaknesses

1. Documentation Limitations: Explanations of certain technical details could be more thorough
2. Performance Data: Lacks concrete performance benchmark data
3. Scalability: Scalability to more complex determinacy results remains unverified
4. User Accessibility: Limited accessibility for non-specialist users

Impact

1. Theoretical Significance:
   • Demonstrates type theory's capability in handling strong set-theoretic results
   • Provides a paradigm for formalizing advanced mathematical topics
2. Practical Value:
   • Establishes foundation for further formalization of descriptive set theory
   • Provides reusable techniques and methods
3. Reproducibility:
   • Complete open-source implementation
   • Detailed technical documentation
   • Good integration with standard libraries

Applicable Scenarios

1. Formalized Mathematics: Applicable to formalizing mathematical theorems requiring strong set-theoretic foundations
2. Game Theory Research: Provides foundation for formalizing infinite game theory
3. Logic Research: Provides tools for studying relationships between determinacy and large cardinals
4. Educational Applications: Can serve as teaching material for advanced mathematical logic courses

References

Key Literature

1. Martin, D. A. (1975): "Borel determinacy" - Original proof of Borel determinacy
2. Martin, D. A. (1985): "A purely inductive proof of Borel determinacy" - Primary reference followed in this paper
3. Gale, D. & Stewart, F. M. (1953): "Infinite games with perfect information" - Original definition of Gale-Stewart games
4. Kechris, A. S. (1995): "Classical descriptive set theory" - Classical textbook on descriptive set theory

Summary: This is an important work in the field of formalized mathematics, successfully formalizing a profound theorem requiring strong set-theoretic foundations into the type-theoretic framework. The paper not only contributes technical innovations but also provides valuable experience and methods for future related work. Despite some limitations, its pioneering contributions and high-quality implementation make it an important milestone in formalized mathematics.