A formalization of Borel determinacy in Lean

Imagine a giant, infinite game of chess played on a board that never ends. Two players take turns making moves forever. The rules are simple: if the infinite sequence of moves they create matches a specific pattern (the "payoff set"), Player 0 wins; otherwise, Player 1 wins.

The big question mathematicians have asked for decades is: Is this game fair? In other words, does one player always have a "perfect strategy" that guarantees a win, no matter how the other player plays?

This paper is about a mathematician named Sven Manthe who used a computer program called Lean to prove that for a very specific, complex class of these games (called "Borel games"), the answer is yes. One player always has a winning strategy.

Here is a breakdown of what he did, using some everyday analogies.

1. The Computer Proof (The "Digital Architect")

Usually, proving things in advanced math is like writing a long essay. But Manthe didn't just write an essay; he built a digital fortress. He used a theorem prover (Lean) which is like a super-strict robot architect. You can't just say "it's obvious"; you have to hand the robot every single brick and show exactly how it fits. If there is even one tiny gap in your logic, the robot refuses to build the wall.

Manthe successfully built a proof that Borel games are "determined" (meaning someone always wins). This is a big deal because these games are incredibly complex, and proving they are fair requires a massive amount of logical heavy lifting.

2. The Strategy: "Unraveling the Knot"

The proof didn't try to solve the game directly. Instead, Manthe used a concept called "unravelability."

The Analogy: Imagine a tangled ball of yarn (the complex game). It's hard to see the pattern. To solve it, you don't just stare at the knot; you pull the yarn apart and lay it out on a table in a straight line.
The Math: Manthe showed that for these complex games, you can "unravel" them into a simpler, straight-line version (a "clopen" game) where the winner is obvious immediately. If you can prove the simple version is fair, then the original tangled version must be fair too.

3. The Hurdle: "The Infinite Ladder"

The tricky part was that Borel games are built up in layers, like a fractal or an infinite ladder. To prove the whole thing is fair, you have to prove it for every single rung of the ladder.

The Problem: In the original proof by the mathematician Donald Martin (from 1975), he used a method called "transfinite induction." Imagine trying to climb a ladder that has an infinite number of rungs, but the rungs keep changing shape as you go up. It's very hard to keep track of which rung you are on.
Manthe's Fix: Instead of climbing rung-by-rung, Manthe used a category theory approach. Think of this as building a scaffolding around the ladder. He created a system where he could look at the whole ladder at once and see that the "stability" of the lower rungs guarantees the stability of the upper ones. He replaced the messy, step-by-step climbing with a smooth, structural view of the whole building.

4. The Technical Twist: "The Strict vs. The Lazy"

One of the most interesting parts of the paper isn't the math itself, but how Manthe programmed it.

In the world of computer math (Lean), there are two ways to handle a function that doesn't always work (a "partial function"):

The "Junk Value" Method (The Lazy Way): If the function doesn't apply, you just force it to return a dummy answer like "0" or "null." It's like a vending machine that gives you a free soda if you put in the wrong coin. It's easy for the computer to handle, but it's mathematically "messy."
The "Strict Domain" Method (The Strict Way): You only allow the function to run if the input is valid. If you try to put in a wrong coin, the machine doesn't even start; it just says "Error: Invalid Input."

Manthe chose the Strict Way.

Why? It matches how human mathematicians actually think. We don't say "if the strategy doesn't exist, it's zero." We say "this strategy only exists for these specific positions."
The Cost: This made the computer work much harder. The robot architect had to constantly check, "Is this input valid?" before doing anything. It slowed things down and required Manthe to write special "magic spells" (tactics) to help the computer keep track of these validity checks.
The Benefit: The proof is much cleaner and closer to the original human intuition. It proves that you can do rigorous math this way, even if the computer finds it annoying.

5. Why Does This Matter?

For Math: It's the first time a proof of this complexity (Borel determinacy) has been fully verified by a computer. It's a milestone.
For Computer Science: It shows that we can use computers to verify the most abstract, high-level math, not just simple arithmetic.
For the Future: It suggests that in the future, we might be able to use computers to prove even harder math problems, provided we are willing to be as precise as the robot architect.

Summary

Sven Manthe took a famous, incredibly difficult math proof about infinite games, translated it into a language a computer could understand, and forced the computer to check every single step. He had to invent new ways to help the computer handle "validity checks" and "infinite structures," proving that even the most abstract mathematical truths can be built brick-by-brick in a digital world.

Here is a detailed technical summary of the paper "A formalization of Borel determinacy in Lean" by Sven Manthe.

1. Problem Statement

The paper addresses the formalization of Borel determinacy, a fundamental theorem in descriptive set theory stating that every Gale-Stewart game with a Borel payoff set is determined (i.e., one player has a winning strategy).

Context: While Borel determinacy is provable in ZFC (Zermelo-Fraenkel set theory with the Axiom of Choice), its proof is notoriously complex, requiring a much larger fragment of ZFC than most standard theorems.
Challenge: No class of games beyond closed sets had been formalized in a proof assistant prior to this work. The complexity arises from the need for transfinite induction, inverse limits of games, and the handling of partial functions (strategies undefined for certain positions).
Goal: To implement a complete proof of Martin's theorem in the Lean 4 theorem prover, utilizing the mathlib library, while navigating the specific constraints of type theory versus set theory.

2. Methodology

The formalization follows the structure of Donald Martin's "purely inductive proof" (specifically the presentation in [Mar85]), adapted for the Lean 4 environment.

A. Theoretical Framework

Unravelability: Instead of proving determinacy directly via induction on the Borel hierarchy, the proof establishes a stronger property called unravelability. A game is unravelable if it can be mapped to a clopen game via a "covering."
Universal Unravelability: The author introduces a strengthened concept, universal unravelability, to facilitate the proof. This allows the set of unravelable games to form a $\sigma$ -algebra, enabling the handling of countable unions without explicit transfinite induction on ordinals.
Categorical Approach: The proof utilizes a category $\mathcal{C}$ of trees and morphisms. The handling of countable unions involves constructing an inverse limit of games. The author proves that the limit of a cofiltered system of trees preserves the necessary "fixing" properties levelwise.

B. Formalization Techniques in Lean

Representation of Sequences: Finite sequences are represented as lists (using mathlib's API). Unlike some formalizations that reverse lists to match tree notation, this work maintains the standard order where the first move is the first element of the list.
Strategies: The author defines strategies as functional strategies (maps from positions to sets of moves) rather than "strategy trees" (sets of positions).
- Pre-strategies: A weaker notion allowing for "no moves" in a position, used to simplify lemmas.
- Quasi-strategies: Allow multiple moves.
- Functional vs. Tree: Functional strategies were chosen for easier definition (avoiding complex recursion), while strategy trees were used for defining winning conditions. A canonical surjection connects the two.
Partial Functions: The project deviates from the mathlib convention of using "junk values" (total functions with a default value for undefined inputs). Instead, it uses dependent types (functions defined only on a specific domain $P(x)$ $P (x)$ ).
- Rationale: This mirrors informal mathematics more closely and simplifies rewriting operations, as hypotheses about the domain are carried automatically with the term.

C. Automation and Tactics

Arithmetic: A custom tactic was developed to handle parity checks (e.g., determining if a sequence length is even/odd) by unfolding list lengths and invoking Lean's omega (Presburger arithmetic solver).
Fixing Properties: To manage the requirement that a map is " $k$ -fixing" (bijective on the first $k$ levels), the author used Lean's typeclass inference. A typeclass Fixing associates a maximal $k$ with a function, allowing Lean to automatically infer the necessary fixing properties for inverse functions.
Performance Optimization: To avoid exponential blowup in proof term sizes caused by nested dependent hypotheses, the author implemented a metaprogram (abstract or as_aux_lemma) that eagerly abstracts proof terms into lemmas.

3. Key Contributions

First Formalization Beyond Closed Sets: This is the first proof assistant formalization of determinacy for any class of sets larger than closed sets (specifically, all Borel sets).
Proof of Martin's Theorem: The code (approx. 5,000 lines) formalizes the full inductive proof of Borel determinacy, including the construction of the inverse limit of games and the verification of the lifting conditions.
Category Theoretic Lemma: The author formalized the existence of limits in the category of trees and proved that the projection maps preserve the "levelwise fixing" property, a crucial step for handling countable unions of games.
Dependent Types vs. Junk Values: The paper provides a comparative analysis of implementing partial functions. It argues that while mathlib prefers "junk values" for simplicity in rewriting, dependent types are superior for complex mathematical structures like strategies, provided that automation (like simp and custom tactics) is tuned to handle them.
Metaprogramming Solutions: The development of tools to handle the performance costs of nested dependent types (specifically the abstract tactic) offers a solution to a known bottleneck in Lean formalizations involving partial functions.

4. Results

Successful Verification: The theorem "Every Borel game is determined" was successfully proven in Lean 4.
Code Structure: The project consists of roughly 5,000 lines of code. The foundational definitions (games, trees, strategies) constitute less than half; the majority is dedicated to the proof of unravelability and the limit construction.
Consistency: The formalization confirms that Borel determinacy holds in Lean's type theory (which is equiconsistent with ZFC + $n$ inaccessible cardinals) using the same logical steps as in ZFC, without needing additional axioms beyond those required for the set-theoretic proof.

5. Significance

Descriptive Set Theory: This work marks a significant milestone in the formalization of advanced set theory. It bridges the gap between finite game theory (Zermelo's theorem) and infinite game theory involving complex Borel sets.
Proof Assistant Capabilities: It demonstrates that Lean 4 and mathlib are capable of handling highly non-trivial proofs involving inverse limits, category theory, and complex inductive arguments, pushing the boundaries of what has been formalized.
Methodological Impact: The paper challenges the prevailing "junk value" convention in mathlib for partial functions. By successfully using dependent types, it suggests that future libraries could adopt a more mathematically natural approach to partiality, potentially improving the readability and maintainability of formal proofs in analysis and topology.
Future Work: The formalization lays the groundwork for tackling stronger forms of determinacy (e.g., analytic determinacy) which require large cardinal axioms, and for building a comprehensive library of descriptive set theory within Lean.

In summary, Sven Manthe's paper is a rigorous technical achievement that not only verifies a deep theorem in set theory but also refines the methodology of formalizing partial functions and complex limits in dependent type theory.