A formalization of Borel determinacy in Lean
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". Final version, to appear in Annals of Formalized Mathematics
Fields of Study & Subjects
Organizational Management and Leadership
Operations Management Techniques
Business Process Modeling and Analysis
Publication details
- Journal / source
- Annals of Formalized Mathematics
- Volume
- Volume 2
- Publication date
- 13 March 2026
- Language
- EN