Formalizing Class Field Theory

Abstract: Class field theory is one of the big achievements of twentieth-century number theory. This talk describes ongoing work to formalize class field theory in Lean, with a focus on progress made during a CMI workshop in July 2025. I will also share reflections on the workshop from the perspective of a participant.

logic in computer sciencemathematical softwarenumber theory

Audience: general audience

( slides | video )

Lean Together 2026