Abstract
Recent advances in artificial intelligence are rapidly changing how mathematics is done. Systems can now generate conjectures, proof sketches, and even complete arguments at a scale and speed that was not possible before. This shift challenges a long-standing assumption: that the main difficulty in mathematics lies in finding proofs. Instead, as proof generation becomes easier, verification becomes the central bottleneck. How can we trust results produced by increasingly powerful AI systems?
In this talk, I will argue that formal verification provides a natural answer to this challenge, by representing proofs in a fully machine-checkable form where every logical step is explicitly justified. I will introduce Lean 4, a modern proof assistant based on dependent type theory, and explain how it treats propositions as types and proofs as programs, allowing verification to reduce to type checking. I will highlight recent developments showing that formalization is becoming significantly faster, and that it is starting to reach the level of mainstream research mathematics. Finally, I will briefly discuss an early-stage initiative to build a formalization library for computational economics, with the goal of bringing game theory, mechanism design, and social choice into a machine-verifiable framework.
Time
Wednesday, Apr.15, 14:00--15:00
Speaker
Xiaohui Bei is an Associate Professor in the Division of Mathematical Sciences at Nanyang Technological University. He obtained his Ph.D. from Tsinghua University in 2012. His research interests include topics in resource allocation, computational economics, and general algorithm design. He has published more than 50 publications at top-tier computer science conferences and journals. He is also the recipient of the Microsoft Research Asia Fellowship and the Nanyang Assistant Professorship.
Room
Room 104
