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

A mechanized proof system of the third generation calculus in Coq

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

Based on the proof assistant Coq, a formal verification of the third generation calculus theory advocated by Academicians Qun Lin and Jingzhong Zhang is completely implemented, including Coq descriptions of all the definitions and theorems in Jingzhong Zhang’s paper entitled "A new way viewing the foundation of calculus". A proof code of all the theorems is given without exception, and all the formalization processes have been verified by Coq. The formal proof demonstrates that the Coq-based mechanized proof has the characteristics of readability and interactivity. The proof process is standardized, rigorous and reliable. This paper is an attempt of the idea that researchers learn, understand, construct, and even educate mathematics by computer assistant.