Formal mathematics—representing mathematics in such a way that computers can verify proofs—has flourished in the last few years as a large community of mathematicians strive to formalize modern mathematics in the Lean Theorem Prover. A major driver of the recent renaissance has been the observation that computers are rapidly becoming more capable, and that as a consequence, the value of explaining our problems to them is growing rapidly as well. Mathematicians using Lean have already written dozens of creative programs to automatically find proofs in various domains, but they have only barely scratched the surface of what is possible. To realize the full potential of computers in mathematics, we must empower mathematicians to implement not only their low-level techniques but also their higher-level problem solving strategies. To drive progress, we propose a grand challenge: develop a program that can win the International Mathematical Olympiad (IMO).
Zoom Link: https://washington.zoom.us/j/99706998012
Daniel Selsam is a Senior Researcher at Microsoft Research. He completed his PhD at Stanford University in Computer Science in 2019.