随着时代发展变革,计算机技术发展势如破竹,人工智能就是典型例证。机器定理证明是人工智能的重要内容,其起源可追至莱布尼茨时代,涉及计算机、数学、逻辑学等多个学科。自动定理证明技术旨在实现计算机自动推理证明,随着时间推移,交互式证明工具也称证明助手应运而生。Coq是一种国际上主流的交互式证明工具,依赖其严谨性、可读性、可信性等特点,基于计算机语言Gallina,合法命名与代码规范实现数学定理的证明或系统安全性验证。通过人机交互的方式,实现计算机协助人完成数学定理的推理过程。数学定理形式化研究具有重要意义,不仅可以推动形式化数学的发展,而且利于读者对数学定理有更深刻的理解。微积分的出现,对近代科学的发展具有里程碑的意义。无论对数学还是物理学等科学都起到了重要作用,研究牛顿-莱布尼茨公式对微积分系统的建立具有重要意义。本文将以华东师范大学数学系编写的《数学分析》为理论依据,实现微积分系统中的数学定理形式化。牛顿-莱布尼茨公式建立了微分与积分之间的联系。本文基于交互式证明工具Coq,从构建系统中底层——实现集合与函数形式化出发,首先对微积分基础内容实现形式化证明,对实数、数列极限、函数极限和连续函数形式化描述,其后在实现导数与微分、拉格朗日中值定理、定积分形式化的基础上,实现牛顿-莱布尼茨公式的形式化。