基于Coq的第三代微积分机器证明系统

摘要

本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分没有极限的微积分理论构架的形式化验证,包括对张景中等发表的题为微积分基础的新视角"论文中全部定义和定理的Coq描述.进而,对定理无例外地给出Coq的机器证明代码,所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠.本文是实践研究人员利用计算机学习、理解、构建乃至教育现代数学理论的一个尝试.