时间：2025年9月30日10:00-11:00

地点：线上（腾讯会议：541-455-035）

题目：智能数学推理：形式化与定理证明

摘要：本报告探讨通过数学形式化推动智能数学推理的技术路线。与传统依赖直觉的证明方式不同，形式化要求每一步都经过严格论证，具有验证可靠性高、定理可复用、支持模块化思维、可自动化验证等优势。我们将介绍数学优化形式化进展和在线协作ReasLab IDE，随后阐述利用Lean核心表达式树实现基于树状结构的前提选择，通过状态链将自然语言证明翻译为形式化证明方法，以及从结构到实例的定理自动形式化框架。

主讲人简介：文再文，北京大学北京国际数学研究中心长聘教授，北京大学博雅特聘教授，主要研究最优化算法与理论、机器学习和人工智能。2016年获中国青年科技奖。2020年获国家万人计划科技创新领军人才，入选2023年度教育部CJ学者特聘教授，现为JSC, JORSC和CSIAM-AM等期刊编委，中国运筹学会副理事长。主编的《最优化方法与理论》入选教育部101计划核心教材，该系列教材累计印刷13次3.2万余本，得到了北大和清华等超百所高校采用。