报告题目：实数公理系统相容性和范畴性的形式化

报告人：郁文生

报告摘要：数学定理的机器证明是人工智能基础理论的深刻体现。国际著名的法国布尔巴基学派引进数学结构的概念，基于序、代数和拓扑三大结构统一构建数学。利用计算机证明辅助工具，可以完整构建布尔巴基数学三大母结构的形式化系统。该系统可方便地应用于拓扑学和代数学理论的形式化构建。本报告介绍如何实现读者跟随计算机学习、理解、构建、教育乃至发展现代数学科研与教学的尝试。

报告人简介：郁文生，1998 年毕业于北京大学，获理学博士学位。现为北京邮电大学，教授，博士生导师，天地互联与融合北京市重点实验室副主任，中国仿真学会智能物联系统建模与仿真专业委员会副主任委员、中国仿真学会理事、北京市人工智能学会常务理事、中国自动化学会控制理论专业委员会委员等。曾任中国科学院自动化所研究员、博士生导师，华东师范大学教授，博士生导师，新疆维吾尔自治区天山学者等。2013年获杨嘉墀科技奖。2017年获吴文俊人工智能自然科学奖。2020、2021年两次获“华罗庚-吴文俊”出版基金资助，科学出版社出版专著《公理化集合论机器证明系统》和《分析基础机器证明系统》。现主持国家自然科学基金重点项目“基于Coq 的布尔巴基数学机器证明系统及其应用”。在系统鲁棒控制理论、时滞系统稳定性分析、线性系统同时镇定及数学定理机器证明等方面做出一系列创新性成果，在《中国科学》、《科学通报》、《IEEE Trans.》系列等国内外重要学术刊物及国内外重要学术会议发表论文150 余篇。曾应邀赴澳大利亚墨尔本大学作高级访问学者。曾多次赴美国、英国、澳大利亚、西班牙、日本及中国香港等国家和地区参加国际性学术会议。目前研究兴趣为数学定理机器证明与人工智能。

报告时间：7月6日15:20-16:50

报告地点：腾讯会议8896574734

报告邀请人：院长

主办单位：188bet 初回入金ボーナス

撰稿：陈凤芹

初审：陈凤芹

复审：刘春晗

终审：院 长