Can Machines Do Mathematics?

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 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? Johan Commelin explores the rapid evolution of AI in mathematics, combining concrete examples with historical context. We trace the path from early experiments to recent breakthroughs, highlighting both the strengths and limitations of these systems. Finally, we consider what the future might hold in five or fifty years, and discuss how the mathematical community can help shape these technologies while preserving its core intellectual values.

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.

35th Johann Bernoulli Lecture
The Johann Bernoulli Lecture is an annual event initiated by the Johann Bernoulli Stichting voor de Wiskunde in honour of the mathematician Johann Bernoulli. It features distinguished speakers who present lectures on various topics in mathematics and related fields. This edition is a collaboration between The Johann Bernoulli Stichting, het Koninklijk Genootschap voor de Natuurkunde (KNG) and Studium Generale Groningen. 

Note: this lecture was previously announced with a different speaker, who is unfortunately unable to attend due to unforeseen circumstances. Johan Commelin has kindly agreed to hold the lecture instead.