活动名称：数学形式化简介

时间：2025年6月6日16:00

地点：汇贤楼数学科学学院122学术报告厅

主讲人：文再文

邀请人：杨新民

主办单位：数学科学学院

主讲人简介：文再文，北京大学北京国际数学研究中心长聘教授，北京大学博雅特聘教授，主要研究最优化算法与理论及其在机器学习、人工智能中的应用。2016年获中国青年科技奖。2020年获国家万人计划科技创新领军人才，入选2023年度教育部长江学者特聘教授，现为JSC, JORSC和CSIAM-AM等期刊编委，中国运筹学会副理事长。

活动简介：与依赖于直觉的传统数学证明方法不同，数学形式化要求每一步都经过严格的论证，确保没有任何逻辑上的漏洞或错误。这种方法具有多种优点：提供了对证明正确性的高度信心；已证明的定理和引理可以在其他证明中重复使用，从而鼓励模块化的思考方式；可以自动化证明的某些步骤；由于每一步都明确定义，更容易看出哪里做了特定的假设或采用了哪种逻辑推理。本报告简要介绍数学形式化基础知识，以及在数学优化形式化方面的一些进展。