Abstract

Computing with or despite the computer

Anne Baanen
Vrije Universiteit

I have recently been collaborating on a project where we compute the class number of quadratic number fields, formally verified as part of the Lean mathematical library. This project took many orders of magnitude more time than the same computation on paper, while Sage finishes in one second. In this talk I want to discuss these three different views of computation and how making them cooperate can create interesting new questions for mathematicians and computer science.