时间：2025年7月30日（星期三）14:00-15:45
地点：E4-233
主讲人: Tao Luo, Shanghai Jiao Tong University
主讲人简介：Dr. Tao Luo is an Associate Professor at the School of Mathematical Sciences/Institute of Natural Sciences at Shanghai Jiao Tong University (SJTU). His research focuses on the mathematical theory of machine learning and materials science. He received his Bachelor's degree in 2012 from Zhiyuan College at SJTU and his Ph.D. from the Hong Kong University of Science and Technology (HKUST) in 2017, where he was awarded the Hong Kong Mathematical Society's Best PhD Thesis Award. From 2017 to 2020, he served as a Golomb Visiting Assistant Professor in the Department of Mathematics at Purdue University. He has made contributions to research in the frequency principle and condensation phenomena in deep learning, as well as the Peierls-Nabarro model, epitaxial growth, and the Cauchy-Born rule in materials science. His work has been published in top international conferences and journals, including the SIAM journal series, Arch. Ration. Mech. Anal., J. Mach. Learn. Res., NeurIPS and ICLR.
讲座主题：AI4Math: Autoformalization and Semantic Evaluation
讲座摘要: Artificial Intelligence for Mathematics (AI4Math) is a rapidly advancing field with significant implications for both academic research and industrial applications. This report examines the evolution of AI-driven mathematical reasoning, tracing the transition from intuitive, natural language-based approaches to the rigorous, verifiable proofs enabled by formal languages. After providing a foundational overview, we conduct a technical survey of three key research frontiers within the formal systems: Automated Theorem Proving, Autoformalization, and Automated Semantic Evaluation. The primary focus is placed on our contributions to the latter two areas, which are crucial for bridging the gap between human mathematical knowledge and machine-verifiable logic.
