Formalising the Krull Topology in Lean

TL;DR

This paper formalizes the Krull topology of infinite Galois extensions in Lean 3, proving its profiniteness, which is essential for Galois representations and the Langlands Program.

Contribution

It provides the first formal proof of the Krull topology's profiniteness within a theorem prover, bridging abstract algebra and formal verification.

Findings

Formalization of Krull topology in Lean 3

Proof of its profiniteness within the theorem prover

Enabling formal reasoning about Galois representations

Abstract

The Galois group of an infinite Galois extension has a natural topology, called the Krull topology, which has the important property of being profinite. It is impossible to talk about Galois representations, and hence the Langlands Program, without first defining the Krull topology. We explain our formalisation of this topology, and our proof that it is profinite, in the Lean 3 theorem prover.