Time: 9:00-17:00, Thursday, July 23 2026
Venue: E14-116
Organizers:
Huayi Chen, Jiedong Jiang, Yijun Yuan
9:00-11:00
Speaker: Riccardo Brasca (Université Paris Cité)
Title: An introduction to formalization of mathematics: why and how to explain research-level mathematics to a computer
Abstract: Formalization is the process of using a computer not merely to perform calculations, but to verify and follow mathematical reasoning step by step. It is becoming an increasingly powerful tool for research mathematicians. Today, even recent and sophisticated mathematical results can be formalized within a reasonable amount of time, and the process is likely to become substantially more efficient in the coming years.
In this talk, I will introduce the practice of formalization through a range of examples and explain how it can increase mathematical understanding in the usual sense and how it can support new forms of collaboration. I will also discuss very recent developments in which ongoing research is formalized almost in real time.
14:30-15:30
Speaker: Rongge Xu (Tsinghua University)
Title：Lean and AI for Formalized Physics
Abstract：Interactive theorem provers such as Lean are beginning to play a broader role in physics. Formalization makes definitions, assumptions, and reasoning steps machine-checkable. It can therefore reveal hidden dependencies, support reusable libraries of physical knowledge, and provide a reliable foundation for AI-assisted reasoning. In this talk, I will introduce recent developments in formalized physics, including the Physlib ecosystem, libraries for quantum information and quantum computing, and emerging applications to quantum field theory and other research-level problems. I will also discuss how large language models and proof agents may assist with formalization, verification, and eventually scientific discovery, with examples from our ongoing work.
16:00-17:00
Speaker: Yang-Hui He (London Institute for Mathematical Sciences, Online)
Title: The AI Mathematician
Abstract: We argue how AI can assist mathematical discovery in three ways: theorem-proving, conjecture formulation, and language processing.
Inspired by initial experiments in geometry and string theory in 2017, we summarize how this emerging field has grown over the past years, and show how various machine-learning algorithms can help with pattern detection across disciplines in theoretical physics and pure mathematics.
At the heart of the programme is the question how does AI will reshape the landscape of future theoretical research.
