Teaching a computer algebraic number theory

Abstract: For most of recorded human history, mathematics has been done with good-old pen and paper. With the advent of modern computers, lightning-fast calculations and large-scale datasets have granted us unprecedented advances in mathematics, both in pure and applied forms. On the other hand, they have merely been algorithmic tools for us to compute with, while lacking the capacity to comprehend and formulate new ideas as we do. I will explore recent attempts at teaching my area of arithmetic geometry to a computer, by formalising fundamental constructions in an interactive theorem prover called Lean.

Mathematics

Audience: researchers in the topic

ANTLR seminar

Series comments: This is the Algebra, Number Theory, Logic and Representation theory seminar.