A Formally-Verified Proof of the Lusin-Novikov Theorem

Descriptive set theory studies the “complexity” of various mathematical objects (sets of reals, functions between topological spaces, equivalence relations, and so on). Under certain assumptions, these objects often have rather rigid structure, admitting so-called “dichotomy” theorems. Indeed, a common structure of theorems in descriptive set theory is proving that either an object is “simple” (e.g. some meaningful quantity is countable), or “complex” in a very predictable way (e.g. containing a Cantor set).

One such theorem that lies at the heart of the field is the Lusin-Novikov theorem, which has a number of distinct but equivalent formulations. The statement investigated in this paper involves continuous functions between sufficiently nice topological spaces. The rough idea of the theorem is that if f : X → Y is continuous (where X and Y are sufficiently nice), we can either write X as a union of countably many pieces on which the restriction of f is injective, or f fails injectivity spectacularly: a single fiber of f contains a Cantor set.

This paper reports on a formalization of the Lusin-Novikov Theorem in the Lean theorem prover. This will hopefully open a lot of doors for formalization in descriptive set theory and related fields, as the Lusin-Novikov theorem is a jumping-off point for future study.

Due to time constraints surrounding this thesis, the proof is not yet on the Lean math library (mathlib), but will be at some point in the future. In the meantime, it can be viewed on GitHub. In section 2, we outline some of the relevant mathematical background needed for the proof, state Lusin-Novikov in math terms, and outline the structure of the proof. In section 3, we go over in detail the proof of Lusin-Novikov and important details in its formalization. In section 4, we outline some room for future work regarding Lusin-Novikov.