Schemes in Lean | Number Theory Lunch Seminar

Abstract

We will discuss how the notion of "schemes" in algebraic geometry can beformalized in the Lean theorem prover

Speaker Intro

Yong Suk Moon joined BlMSA in 2022 fall as an assistant professor. His research area is numbertheory and arithmetic geometry. More specifically, his current research focuses on p-adic Hodgetheory, Fontaine-Mazur conjecture, and p-adic Langlands program. He completed his Ph.D atHarvard University in 2016, and was a Golomb visiting assistant professor at Purdue University(2016-19) and a postdoctoral researcher at University ofArizona (2019 -22).