Recorded 16 February 2023. Maria Ines de Frutos Fernandez of Imperial College London presents "Formalizing Norm Extensions and Applications to Number Theory" at IPAM's Machine Assisted Proofs Workshop. Abstract: Let K be a eld complete with respect to a nonarchimedean real-valued norm, and let L=K be an algebraic extension. We formalize in Lean 3 the proof that there is a unique norm on L extending the given norm on K, and we provide an explicit description of this norm. This is a prerequisite to formalize Local Class Field Theory, which is an essential component in the proof of Fermat's Last Theorem. As an application, we extend the p-adic norm on the eld Qp of p-adic numbers to its algebraic closure Qalg p , and we dene the eld Cp, a p-adic analogue of the complex numbers. Building on the denition of Cp, we formalize the denition of the Fontaine period ring BHT. Both Cp and BHT can be used to detect certain properties of Galois representations. Learn more online at: http://www.ipam.ucla.edu/programs/workshops/machine-assisted-proofs/