报告题目：AI for Mathematics in Lean
报 告 人：Yunzhou Xie
报告时间：2025年9月8日（周一）下午 15:00-16:00
报告地点：藕舫楼725室
主 持 人：张毅 副教授
报告摘要：
Artificial intelligence has recently reached a milestone in mathematical problem solving: in 2025, systems developed by Google DeepMind and OpenAI each achieved gold-medal performance at the International Mathematical Olympiad, solving five of six problems under official grading. This breakthrough highlights AI’s growing capacity for structured reasoning, moving beyond pattern recognition.
In this talk, I will examine how such advances connect to the development of formal mathematics in Lean. I will discuss the role of large language models in proof search, autoformalization, and verification, and illustrate how techniques that enabled Olympiad-level success can be adapted to research mathematics. At the same time, I will outline the current limitations of AI-assisted proof systems and the challenges of translating informal reasoning into formal language. I will conclude with reflections on how a deeper collaboration between mathematicians, Lean, and AI could reshape the practice of pure mathematics.
报告人简介：
Yunzhou Xie is a PHD student of professor Kevin Buzzard in Imperial College London who accomplished several minor projects with him and his phd students to assist his great goal of formalising Fermat Last Theorem in to Lean4 (address : https://github.com/ImperialCollegeLondon/FLT).
欢迎广大师生踊跃参加！
数学与统计学院
江苏省应用数学（南京信息工程大学）中心
江苏省系统建模与数据分析国际合作联合实验室
2025年9月8日
