软件学报

作者：窦国威，郁文生

单位：窦国威，天地互联与融合北京市重点实验室(北京邮电大学 电子工程学院), 北京 10087611,郁文生，天地互联与融合北京市重点实验室(北京邮电大学 电子工程学院), 北京 10087602

关键词：形式化数学;定理机器证明;Coq;数学分析;一元微积分

基金：国家自然科学基金(62476028, 61936008)

形式化数学是一次数学革命,结合定理证明器的数学定理机器证明,不仅是对数学严谨性的一种新标准,更是发展数学的一种新方式.随着世界范围不断有数学难题在计算机辅助下的成功解决,以及各路专家学者对各种数学形式化项目或工程的发起,形式化数学的影响力与日俱增.国际数学家陶哲轩即于2025年5月发起了一个基于定理证明器Lean的数学分析形式化项目,在数学界与计算机界引起广泛影响.本文介绍一项基于定理证明工具Coq的数学分析形式化系统,该系统以华东师范大学数学系编著的《数学分析》为蓝本,在朴素集合论和初等数论及代数知识体系下进行开发,当前,已经实现其上册中一元微积分相关内容的形式化,包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、不定积分、定积分等内容.我们开发的系统严格对应教材内容,全部定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过.读者可以跟随代码学习数学,也能够对照数学理解代码,充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点,实现让读者跟随计算机学习、理解、构建、教育乃至发展现代数学的尝试,提高认识数学、感受数学和欣赏数学的素养.

来源：2026年第9期

《软件学报》期刊编辑部

查看软件学报杂志2026年第9期