Algebra/Topology Seminar

Speaker: Jiedong Jiang

Title: Intro to Formalizing Valuation Theory in Lean

Abstract: In this talk, we will discuss the formalization of the valuation theory in number theory using Lean. We will begin with a brief introduction to the interactive theorem prover Lean and its mathematical library Mathlib. Then we will focus on some concrete examples of the implementation of key definitions from valuation theory in Mathlib, explaining the design behind them. Throughout the talk, we will also discuss several counter-examples and challenges encountered during the formalization process.