Johann Bernoulli lezing 35 - Dr. Johan Commelin, University of Utrecht

Title: Can machines do Mathematics?

Abstract:

When ChatGPT launched in 2022, it showed the world that computers can write poetry, generate images, and hold conversations, but in mathematics it still struggled with simple logic puzzles and long division. Three years later, the picture looks very different, with AIs winning gold medals at the International Mathematical Olympiad and mathematicians publishing papers that credit AI assistants with suggesting key ideas. What happened, and how impressed should we be? This lecture offers a guided tour through one of the fastest-moving stories in recent science. Computers have long helped with calculations, but could they ever take part in the reasoning itself? If mathematics is a language, what happens when computers learn to speak it fluently; and how might this change the way we prove, verify, and communicate mathematics?

With concrete examples and historical anecdotes, we trace the path from pioneering work to recent breakthroughs, and examine what these systems can and cannot do. Along the way we will encounter striking examples, from computer-generated proofs to large collaborative projects formalizing modern mathematics. At the heart of this development are new formal proof languages, which are emerging as a common interface through which humans, automated theorem provers, and machine learning systems can collaborate. The talk concludes with a look ahead: where might this lead, in five years or fifty? And how should the mathematical community guide the development of these technologies while preserving its own intellectual values? This lecture aims to offer honest orientation in a fast-changing landscape.

Short bio:

Johan Commelin is a Dutch mathematician, assistant professor at Utrecht University, leading a research group in fundamental mathematics and director of the Mathlib Initiative. His work focuses on formalizing mathematics with a background in arithmetic geometry. Commelin is driven by the goal of building a comprehensive and fast library of digital mathematics. He is deeply interested in preparing mathematics for the digital era, rethinking how we collaborate, research and teach. Beyond the technical work, he reflects on the values of the mathematical community and how mechanization impacts mathematical culture, advocating for guarding the human aspect of mathematics against the soulless forces of big tech. He is a central figure in the Lean and Mathlib community, contributing to the infrastructure that mathematicians and computer scientists worldwide rely on.

Laudatio: Prof. dr. Bart Verheij (RUG)