Seminar

In this talk, we will explore the practical uses of a proof assistant for mathematicians. In particular, we will learn how to formalize a variety of propositions in the proof assistant Lean 4. Through these examples, we will learn how to convert our familiar strategies into the different proof tactics which have been implemented in Lean. Additionally, we will discuss why they are called proof assistants and the different ways that they make proving things easier. Finally, we’ll touch on some theory behind proof assistants and their role in modern mathematics.

In this talk, we will first discuss the motivations for motivic classes coming from point counting over finite fields. Then we will give the definitions of the motivic classes of varieties, in particular we explain that an extra relation is needed in finite characteristic. We will introduce symmetric powers and motivic zeta functions that are universal versions of local zeta functions.

The most skilled mathematicians in the world must also be effective communicators. In the first three years of my Ph.D., I gave seven math talks, all with undergraduate math students in mind. In this talk, I will discuss the benefits of giving undergrad-friendly talks, both for your progress as a Ph.D. student and for preparing to apply to academic jobs. I will offer some advice on topic selection, and then I will share some key principles to keep in mind when making undergraduate-friendly talks, using my own past talks as examples.