皇冠会员登录-浙江中南建设集团

校园门户

数字图书

数字资源（校外访问）

校园邮箱

上网登录

信息公开

领导信箱

皇冠会员登录概览
云之家网页版设置
组织机构
人才师资
- 人才招聘
教育教学
- 本科生教育
- 研究生教育
- 教师教育
- 留学生教育
- 继续教育
学术研究
- 学科建设
- 科研管理
- 科研平台
- 科研动态
- 学术刊物
招生就业
- 本科生招生
- 研究生招生
- 留学生招生
- 继续教育招生
- 就业信息
合作交流
- 国内交流与合作
- 国际交流与合作
重庆国家应用数学中心

校园门户

数字图书

数字资源（校外访问）

校园邮箱

上网登录

信息公开

领导信箱

皇冠会员登录概览
云之家网页版设置
组织机构
人才师资
- 人才招聘
教育教学
- 本科生教育
- 研究生教育
- 教师教育
- 留学生教育
- 继续教育
学术研究
- 学科建设
- 科研管理
- 科研平台
- 科研动态
- 学术刊物
招生就业
- 本科生招生
- 研究生招生
- 留学生招生
- 继续教育招生
- 就业信息
合作交流
- 国内交流与合作
- 国际交流与合作
重庆国家应用数学中心

皇冠会员登录概览
云之家网页版设置
组织机构
人才师资
- 人才招聘
教育教学
- 本科生教育
- 研究生教育
- 教师教育
- 留学生教育
- 继续教育
学术研究
- 学科建设
- 科研管理
- 科研平台
- 科研动态
- 学术刊物
招生就业
- 本科生招生
- 研究生招生
- 留学生招生
- 继续教育招生
- 就业信息
合作交流
- 国内交流与合作
- 国际交流与合作
重庆国家应用数学中心

皇冠会员登录概览
云之家网页版设置
组织机构
人才师资
- 人才招聘
教育教学
- 本科生教育
- 研究生教育
- 教师教育
- 留学生教育
- 继续教育
学术研究
- 学科建设
- 科研管理
- 科研平台
- 科研动态
- 学术刊物
招生就业
- 本科生招生
- 研究生招生
- 留学生招生
- 继续教育招生
- 就业信息
合作交流
- 国内交流与合作
- 国际交流与合作
重庆国家应用数学中心

校园门户
数字图书
数字资源（校外访问）
校园邮箱
上网登录
信息公开
领导信箱

综合新闻
通知公告
学术动态
学术预告
媒体重师
重师故事
重师观像
光影集萃
图说重师
云之家网页版经纬
加快打造西部地区师范名校
深入学习贯彻党的二十届四中全皇冠集团娱乐网站精神

网站首页

综合新闻
通知公告
学术动态
学术预告
媒体重师
重师故事
重师观像
光影集萃
图说重师
云之家网页版经纬
加快打造西部地区师范名校
深入学习贯彻党的二十届四中全皇冠集团娱乐网站精神

当前位置：

网站首页 > 学术预告 > 正文

数学形式化简介

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

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

地点：汇贤楼数学科学云之家网页版122学术报告厅

主讲人：文再文

邀请人：杨新民

主办单位：数学科学云之家网页版

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

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