随着计算机技术的发展,数学机械化受到了越来越多的关注,形式化数学是数学机械化领域的一个重要分支,即通过形式化的方式描述数学中的定义、定理等内容,并完成相应的证明,使得定理的证明能够方便地利用计算机来验证。相比于传统的人工证明,形式化证明有着高可信性的特点。近年来随着Coq,Isabelle等证明辅助工具的出现,形式化数学的研究也取得了长足的进展,并且国内外的相关学者也已经启动了许多形式化证明的工程,使得相关成果进一步丰富。基础理论的形式化对形式化数学的研究尤为重要。级数理论是数学分析中的重要内容,也是其他数学理论的基础,并且对物理、天文等学科的发展起到了重要作用。本文借助于交互式定理证明工具Coq实现级数理论的形式化证明,主要工作内容如下:（1）给出集合、函数、数列等相关概念的形式化描述。并完成极限唯一性、单调有界定理、Cauchy收敛准则、幂函数等相关定理的形式化证明,为级数理论的证明作铺垫。（2）通过数列表示出数项级数,并完成数项级数的Cauchy准则、等比级数、正项级数判别法、Leibniz判别法、绝对收敛级数等相关定理的形式化证明。（3）通过函数列表示出函数项级数,给出函数列以及函数项级数一致收敛的形式化定义,并完成一致收敛的判别以及性质、Cauchy准则等相关定理的形式化证明。最后完成幂级数相关的Abel定理、和函数连续性、Taylor公式、幂级数展开等的形式化。本文的所有代码均已在Coq中验证通过,证明过程充分体现了Coq的规范、严谨、可靠的特点。