Formalizing Number Theory in Lean

Mathematical formalization is the process of digitizing mathematical definitions and results using a "proof assistant", a computer program capable of checking logical statements against a set of inference rules and some basic axioms. In recent years, the community of mathematicians working on formalization has grown rapidly and has reached milestones that demonstrate the ability to formalize results at the frontier of knowledge. Proof assistants have applications to mathematical research, teaching, and communication.

After a brief introduction to formalization, I will present several of my  formalization results in the Lean interactive proof assistant, from sub-areas of number theory including class field theory, p-adic Hodge theory, and the theory of Drinfeld modules.