智能数学推理：形式化与定理证明
报告专家：文再文教授（北京大学）
报告时间：9月2日（星期二）上午10:00-11:00
报告地点：国家天元数学西南中心516
报告摘要：
本报告探讨通过数学形式化推动智能数学推理的技术路线。与传统依赖直觉的证明方式不同，形式化要求每一步都经过严格论证，具有验证可靠性高、定理可复用、支持模块化思维、可自动化验证等优势。我们将介绍数学优化形式化进展和在线协作ReasLab IDE，随后阐述利用Lean核心表达式树实现基于树状结构的前提选择，通过状态链将自然语言证明翻译为形式化证明方法，以及从结构到实例的定理自动形式化框架。
专家简介：
文再文，北京大学博雅特聘教授，主要研究最优化算法与理论、机器学习和人工智能。与合作者开拓了正交约束优化研究领域，推动了流形优化的发展，提出了求解非光滑优化的原始-对偶半光滑牛顿法，研发了OptSuite优化软件和ReasLab在线形式化平台。主编的《最优化方法与理论》入选教育部101计划核心教材，该系列教材累计印刷2.6万余本，得到了北大和清华等超百所高校采用。获中国青年科技奖，入选国家高端人才计划科技创新领军人才和教育部重要人才计划特聘教授。现任中国运筹学会副理事长。
邀请人：连增
