Borel Games Enter a Proof Assistant: What Lean’s 2026 Determinacy Formalization Establishes

A strategy must survive every reply

A strategy is more than a promising sequence of moves. It tells a player what to do after every legal finite history at which that player acts. Calling a strategy winning means that every complete play consistent with those instructions wins, whatever the opponent chooses. The order of these quantifiers matters: there exists one strategy that works against all responses. A different response to each fully revealed opponent plan would describe a weaker and potentially misleading claim.

Consider an original toy rule: the first player wins exactly when their opening number is even. Choosing zero settles the outcome before the opponent acts, despite the formally infinite continuation. Now replace that rule with one requiring infinitely many zeros somewhere in the sequence. A finite prefix can never certify that there will be infinitely many, although a player controlling alternate turns can enforce this particular condition by repeatedly choosing zero. The examples separate a condition’s logical complexity from the difficulty of finding a strategy.

Two players cannot both have winning strategies in this setting. If both allegedly did, let them follow those strategies against each other. Their instructions recursively determine one legal infinite play. The first strategy says that play belongs to the first player’s payoff set; the second says it belongs to its complement. Those conclusions conflict. The difficult part of determinacy is therefore existence of at least one winning strategy, rather than uniqueness of the winner once such a strategy exists. This short argument also shows why the definition must quantify over every play consistent with a strategy: success against one selected opponent would not support the contradiction.

What the Borel restriction actually controls

The space of infinite sequences comes with a natural topology. Specifying the first few entries gives a basic neighborhood: all sequences sharing that prefix. An open winning condition has a useful interpretation. Whenever a sequence satisfies it, some finite initial segment already guarantees satisfaction. Closed conditions have the dual property that failure becomes visible after finitely many moves. Borel sets are obtained from open sets using complements and countable unions, iterating these operations as needed.

The infinitely-many-zeros example can be written without examining a completed infinite list. For every starting position N, there must be a later position containing zero. For fixed N, the existence of such a later position is an open condition: a sufficiently long prefix exhibits the zero. Intersect those open sets over all natural N. Countable intersections are available because intersection can be expressed using complements and unions. This demonstrates why Borel conditions encompass genuine infinite behavior, beyond games whose outcomes become known at a uniformly bounded time.

Why finite-game intuition needs a stronger tool

In a finite game tree, one can label terminal positions and work backward. At a player’s turn, a position is winning if an allowed move reaches a favorable position. An infinite tree may have no terminal positions to initialize that calculation. Nor can one simply prove determinacy for some winning sets and assume it survives every union. Strategies that work for separate alternatives need not combine into a strategy that knows which alternative to pursue while play is still unfolding.

Manthe’s paper therefore follows Martin’s inductive approach through a stronger property, universal unravelability. The construction replaces a game with a related game whose winning condition is easier to analyze, while retaining a way to transport strategies back. The formalization strengthens the invariant so that it behaves correctly under the operations generating Borel sets. Category-theoretic bookkeeping helps handle compatible maps between trees. These are changes to how the argument is organized for checking, not a claim that the computer discovers a winning move by simulating every possible future.

Legal histories become mathematical data

One can encode a game using a tree of finite histories. Every prefix of a legal history must also be legal, and the setting must ensure that permitted play can continue. That choice prevents an unannounced dead end from silently changing an infinite game into a finite one. A branch is an infinite sequence whose every finite prefix belongs to the tree. A payoff set then selects the branches won by the first player. Separating legality from payoff makes it possible to discuss the same move structure with several different winning conditions.

A proof assistant turns informal domain restrictions into concrete obligations. A strategy cannot merely return an arbitrary number if some numbers are illegal after the present history. Either its output carries evidence of legality, or legality must appear as a separately proved condition. This is analogous to defining division only where a denominator is nonzero, but the objects here are histories and continuations. The resulting types are not decorative labels. They decide which compositions are meaningful and which apparent shortcuts still require a proof.

An existence theorem is not an executable oracle

The result asserts that a winning strategy exists under the stated hypotheses. It does not provide a general practical algorithm that reads an arbitrary description of a Borel condition and promptly prints an optimal strategy. To see the distinction in an elementary setting, the assertion that a nonempty set contains an element says nothing about the cost of locating one from a compressed description. An infinite game adds further issues: the winning instructions themselves may encode information that a finite program cannot conveniently recover.

Machine checking also addresses a different question from foundational strength. A checker verifies a derivation using the rules and assumptions of its logical framework. It does not establish that framework’s consistency merely by accepting the derivation. Manthe discusses how Borel determinacy fits within Lean’s foundations and distinguishes it from stronger determinacy principles. Readers should therefore resist two opposite overstatements: that checking makes all foundations unnecessary, and that a foundation-sensitive theorem somehow becomes meaningless when expressed using types rather than set-theoretic notation.

What a reader can now inspect

The published article identifies a specific theorem and the public repository supplies its formal development. That pairing permits a more detailed audit than a headline announcing computer verification. A reader can compare the formal notion of winning with the ordinary quantifier pattern, inspect the payoff restrictions, and trace which auxiliary results the proof calls. Reusing the definitions in another project offers an additional test of whether they capture useful mathematical concepts. Build reproduction remains a separate task; this article reports the published work and does not claim to have rerun its Lean toolchain.

A promising next step would be libraries that make different classes of infinite games easy to compare without repeatedly rebuilding the same foundations. Another is clearer presentation of what a formally proved strategy-existence theorem supplies to an analyst, logician, or theoretical computer scientist. Neither requires pretending that every statement about infinity becomes computable. The 2026 publication instead illustrates a concrete advance: a delicate theorem about all possible replies can be represented with enough precision that its proof becomes an inspectable mathematical artifact.