形式化数学前沿：从工程实现到人工智能辅助

时间：2026年1月23日

地点：北京国际数学研究中心（BICMR）镜春园78号 77201会议室

会议简介

本次会议聚焦形式化数学领域的技术突破与范式转型，系统梳理当前核心挑战与前沿方向。议程分为三大模块：

第一模块：形式化数学的工程化实践

深入解析交互式定理证明器（ITP）的底层架构设计原理，涵盖核心模块的实现策略与优化路径。通过剖析主流工具（如Lean、Coq）的工程实现原理，探讨如何平衡形式化严谨性与系统性能的关系。

第二模块：标准化评估体系构建

针对前沿代数领域，构建多层次形式化基准测试体系。该体系将覆盖证明复杂度、验证效率、代码可维护性等关键指标，为领域技术发展提供量化评估框架。

第三模块：AI驱动的范式革新

• 理论突破：展示形式化深度理论研究的最新进展，以交换代数中经典定理的机械化为典型案例，解析AI辅助证明的技术路径

• 人机协同：探讨定理证明过程中的人机协作模式，重点分析AI在引理发现、路径规划、错误修正等环节的赋能效应

• 现场展示：展示一个AI辅助证明工具.

本次会议贯通理论、实现与AI辅助三大维度，构建跨学科学术对话平台，推动形式化数学从专家领域向工程化、智能化方向跨越发展。

组织委员会

陈华一（西湖大学）

肖梁（北京大学）

王善文（太阳集团tyc151）

于鹏（太阳集团tyc151）

报告人

董安杰（香港中文大学（深圳））

何婉仪（北京大学）

关乃粼（北京大学）

王语桐（北京大学）

主办单位

北京国际数学研究中心

太阳集团tyc151明理书院、太阳集团tyc151

国家自然科学基金委员会