A formalization of Borel determinacy in Lean

Fuente: arXiv
Salvato in:
Dettagli Bibliografici
Autore principale: Manthe, Sven
Natura: Preprint
Pubblicazione: 2025
Soggetti:
Accesso online:
Tags: Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
_version_ 1866917349072830464
author Manthe, Sven
author_facet Manthe, Sven
contents 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".
format Preprint
id arxiv_https___arxiv_org_abs_2502_03432
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle A formalization of Borel determinacy in Lean
Manthe, Sven
Logic
68V20, 03E60
F.4.1
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".
title A formalization of Borel determinacy in Lean
topic Logic
68V20, 03E60
F.4.1
url https://arxiv.org/abs/2502.03432