A formalization of Borel determinacy in Lean

TL;DR

This paper formalizes Borel determinacy within the Lean 4 theorem prover, providing a rigorous proof of Martin's theorem that Borel games are determined, based on Gale-Stewart games.

Contribution

It offers the first formal proof of Borel determinacy in Lean 4, following Martin's inductive approach, enhancing formal verification in set theory and game theory.

Findings

Successful formalization of Gale-Stewart games in Lean 4

Proof of Borel determinacy following Martin's theorem

Establishment of a foundation for further formalized results in descriptive set theory

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".