A formalisation of Gallagher's ergodic theorem

TL;DR

This paper formalizes Gallagher's ergodic theorem within the Lean theorem prover, providing a foundational step for proving the Duffin-Schaeffer conjecture and highlighting the theorem's significance in metric number theory.

Contribution

It introduces a formal proof of Gallagher's ergodic theorem in Lean, enabling rigorous computer-verified reasoning in metric number theory.

Findings

Formal proof of Gallagher's ergodic theorem in Lean

Supports the proof of the Duffin-Schaeffer conjecture

Enhances reliability of results in metric number theory

Abstract

Gallagher's ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking 'all or nothing' behaviour. We discuss a formalisation of this result in the Lean theorem prover. As well as being notable in its own right, the result is a key preliminary, required for Koukoulopoulos and Maynard's stunning recent proof of the Duffin-Schaeffer conjecture.