Let C+ be a curve of genus at least 2 embedded in its Jacobian and let C- = {-c : c in C+} be the negative embedding. The Ceresa cycle [C+] - [C-] is the simplest example of an algebraic cycle which is trivial in homology but (generally) non-trivial modulo algebraic equivalence. Hyperelliptic curves have trivial Ceresa class, but only recently examples of non-hyperelliptic curves with torsion Ceresa cycle were found.
For more information, please visit the Pitt AWM webpage.
For more information, please visit the Pitt AWM Chapter webpage.
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.