General Math Colloquium: Johan Commelin
math \over human \join computer
Our next meeting of the General Mathematics Colloquium series at the Korteweg-de Vries Institute for Mathematics will be Wednesday, February 5 at 16.00. Johan Commelin (Utrecht University and Lean FRO) will speak about math \over human \join computer.
Event details of
General Math Colloquium: Johan Commelin
- Date
- 5 February 2025
- Time
- 16:00
- Location
- Science Park 904
- Room
- C0.110
Abstract
Humanity has developed many different ways to communicate mathematics, ranging from the very intuitive to the rigorous and precise. In this talk I will explore how we communicate mathematics. Using various examples, I will explain how formal proof languages and computers can enhance the mathematical ecosystem, thereby allowing us to expand the ways in which we practice mathematics.
Note the unusual location!
