Program
April 7, 2026 18F Auditorium, SIMIS, Shanghai
Organizer: Ziran Liu
- Zoom Meeting ID: 893 1693 9565 | Passcode: 697460
Morning Session
09:00–09:05
Shing-Tung Yau
Opening Remarks
09:10–09:55
Yang-Hui He (in person) 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 of how AI will reshape the landscape of future theoretical research.
Bio: Yang-Hui He is a professor of mathematics at the University of London and a member of the London Institute for Mathematical Sciences, as well as a tutor in mathematics at Merton College, Oxford. His research lies at the interface of geometry, number theory, and string theory, with recent emphasis on AI-guided mathematical discovery. His work explores how machine learning can assist in conjecture generation, pattern recognition, and the discovery of mathematical structures across disciplines.
09:55–10:00
Short Break
10:00–10:45
Jeremy Avigad (remote) Reflections on Formalization, Neurosymbolic Reasoning, and the Future of Mathematics
Abstract: In 2002, I formalized the law of quadratic reciprocity in Isabelle with students at Carnegie Mellon. The library was still young; we found and fixed a mistake in the definition of “prime number” on the integers. AI and formal methods for mathematics have come a long way since then. In this talk, I will share a personal perspective on how we got here, reflect on where we stand, and speculate as to how mathematics may change in the years ahead.
Bio: Jeremy Avigad is a professor at Carnegie Mellon University and Director of the Hoskinson Center for Formal Mathematics. He is a leading researcher in mathematical logic, formal verification, and interactive theorem proving. His work focuses on the formalization of mathematics and the development of tools for machine-assisted reasoning, playing a central role in AI for Mathematics.
10:45–10:50
Short Break
10:50–11:35
Leonardo de Moura (remote) Lean: Machine-Checked Mathematics and Verified Programming
Abstract: Lean enables machine-checkable proofs and trustworthy collaboration between mathematicians, programmers, and AI systems. We discuss its impact on mathematics, software verification, and AI.
Bio: Leonardo de Moura is the chief architect and co-founder of the Lean Focused Research Organization and was previously a senior principal applied scientist at Amazon Web Services. He is the creator of Lean and co-creator of the Z3 SMT solver, and his work is foundational in automated reasoning and machine-checked mathematics.
11:35–11:55
Coffee Break
11:55–12:40
Yijun Yuan (in person) Formalization of Non-Archimedean Functional Analysis
Abstract: We formalize spherically complete spaces in Lean 4 and develop applications including Hahn–Banach and orthogonality results in non-Archimedean analysis.
Bio: Yijun Yuan is a postdoctoral researcher at the Institute for Theoretical Sciences at Westlake University. His research focuses on arithmetic geometry, number theory, and Lean-based formalization of advanced mathematics, contributing to the expansion of machine-checkable mathematical knowledge.
Lunch Break
12:40–14:10
Afternoon Session
14:10–14:55
Bin Dong (in person) AI for Mathematics: From Digitization to Automated Reasoning
Abstract: We discuss how AI enables mathematical research and emphasize formalization as the key step toward automated reasoning.
Bio: Bin Dong is a Boya Distinguished Professor at Peking University. His research spans machine learning, scientific computing, and computational mathematics. He has played a leading role in developing AI for Mathematics, particularly in formalization and automated reasoning systems.
14:55–15:00
Short Break
15:00–15:45
Lihong Zhi (in person) Algebraic Reasoning in Formal Mathematics
Abstract: We integrate Lean with symbolic computation systems to enable efficient and verifiable algebraic reasoning.
Bio: Lihong Zhi is a professor at the Academy of Mathematics and Systems Science, Chinese Academy of Sciences, and Director of the Key Laboratory of Mathematics Mechanization. Her work focuses on symbolic computation and automated reasoning, especially bridging formal proof systems with efficient algebraic computation.
15:45–16:05
Coffee Break
Late Afternoon Session
16:05–16:50
Johan Commelin (remote) Mathlib: A Living Library of Machine-Checked Mathematics
Abstract: Mathlib is the largest coherent library of formal mathematics ever built: over 2.1 million lines of Lean code, written and reviewed by more than 750 contributors.
I will explain what makes Mathlib work, as a mathematical artifact, as a community effort, and as infrastructure for AI.
Technically, Mathlib scales through aggressive generality, uniform API design, and continuous refactoring.
Socially, a globally distributed community maintains coherence through careful review and dedicated editorial support.
Crucially, Mathlib is human-curated.
Every definition has been reviewed by expert mathematicians for correctness, generality, and mathematical naturality.
In an age where AI systems increasingly generate formal mathematics, this may be Mathlib’s strongest asset:
when a statement uses Mathlib’s definitions, you know they are not hallucinated; they mean what you think they mean.
In the end, that trust is what enables humans and machines to do serious mathematics together..
Bio: Johan Commelin is an assistant professor at Utrecht University and Director of the Mathlib Initiative. His research focuses on formal mathematics, type theory, and large-scale mathematical libraries, playing a key role in the infrastructure of modern theorem-proving systems.
16:50–16:55
Short Break
16:55–17:40
Kevin Buzzard (remote) The Role of Autoformalisation in Mathematics
Abstract: We discuss the importance of formalization and the emerging role of large-scale autoformalization in mathematics.
Bio: Kevin Buzzard is a professor of pure mathematics at Imperial College London. He is a leading advocate of formalization in mathematics and has played a major role in promoting Lean and formal proof methods in research.
Closing
17:40–17:45
Closing Remarks
Registration
This is an invited workshop; for registration or inquiries, please contact zliu (at) simis.cn .
English 
简体中文