A formalization of Borel determinacy in Lean
Logic
2026-03-18 v5
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".
Cite
@article{arxiv.2502.03432,
title = {A formalization of Borel determinacy in Lean},
author = {Sven Manthe},
journal= {arXiv preprint arXiv:2502.03432},
year = {2026}
}
Comments
Final version, to appear in Annals of Formalized Mathematics