Sven Manthe

collaborators

3 papers

math.LO2026

A formalization of Borel determinacy in Lean

Sven Manthe

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…

math.LO2026

The Borel monadic theory of order is decidable

Sven Manthe

The monadic theory of $(R, \leq)$ with quantification restricted to Borel sets is decidable. The Boolean combinations of $F_{I ¨} $ sets form an elementary substructure of the Bo…

math.LO2024

A Cobham theorem for scalar multiplication

Philipp Hieronymi, Sven Manthe, Chris Schulz

Let $I^\pm, I^^{2} \in R_{> 0}$ be such that $I^\pm, I^^{2}$ are quadratic and $Q (I^\pm) \neq = Q (I^^{2})$ . Then every subset of $R^{n}$ definable in both $(\mathbb{R},{<},+,…