The Chebotarev Density Theorem in Lean🔗

This is the mathematical blueprint for the Lean 4 / Mathlib formalisation of the Chebotarev density theorem.

The development proceeds in six arcs: Dirichlet density of a set of primes; the decomposition group, inertia, and Frobenius at a prime; the factorisation of the Dedekind zeta function of an abelian extension into Artin/Dirichlet L-functions; the cyclotomic case of Chebotarev (via Dirichlet's theorem on primes in arithmetic progressions); the reduction of the general abelian case to the cyclotomic one; and finally the full Chebotarev density theorem.

How to read this blueprint. Each node below is a definition or theorem with its mathematical statement and a paragraph-level proof sketch. The dependency graph records which results feed into which. A node is coloured green once the Lean declaration it references (lean := …) is fully proved, blue while it is stated but still contains sorry, and left uncoloured while it is roadmap-only. There is no manual status to maintain: Verso reads it from the Lean side directly.