人工智能研究是当前科技发展的热点和前沿方向,夯实人工智能基础理论尤为重要,数学定理机器证明是人工智能基础理论研究的深刻体现。定理机器证明主要是指借助计算机技术实现数学定理的机器证明,从而在数学推理中实现脑力劳动的机械化。近年来随着计算机技术的发展,尤其一些定理证明辅助工具Coq、Isabella、HOL Light等的出现,数学定理机器证明的研究取得了长足的发展。对于数学理论的形式化来说,实现微积分的形式化更为基础。微积分是数学史上最伟大的成就之一,不仅开启了数学发展的新纪元,对人类科学技术的发展也起到了重要的促进作用。然而,传统微积分中晦涩难懂的极限概念提高了微积分学习的门槛。因此,一直以来国内外均有学者致力于不用极限微积分的研究,并取得了一定的成果。本文基于证明辅助工具Coq,完整实现林群院士和张景中院士等倡导的第三代微积分——没有极限的微积分——理论构架的形式化验证。主要工作包括:1、在Coq库中实数定义的基础上,给出集合、区间、函数等基本定义的形式化描述,为搭建微积分理论的形式化框架做了必要准备。2、严格按照张景中等发表的题为“微积分基础的新视角”一文,实现对一致连续、一致(强)可导、积分系统、积分严格不等式等定义以及估值定理的形式化描述和机器证明。3、在避开极限概念的导数、积分等定义的基础上,实现了微积分的基本定理:函数的单调性与导函数的关系定理、Newton-Leibniz公式、变上限积分可导性以及Taylor公式的机器证明。本文所有形式化过程已被Coq验证,并在计算机上运行通过,体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠。本文是实践研究人员利用计算机学习、理解、构建、教育乃至发展数学理论的一个尝试。