Mizar系统起源于数学定理的机械化证明,它是用于证明和计算数学问题的计算机语言系统,专门用来构建Mizar数学知识库的自动推理校验。Mizar系统拥有世界上最大的数学数据库(MML),其中已经收录1126篇文章,2万多个数学概念,40多万条数学定理,几乎涵盖了数学科学的各个分支。当前,Mizar系统已经从单一定理证明发展到多学科多方面的交叉应用,特别是在自动控制、声音和图像识别等研究领域有着更为广泛的应用。本文首先介绍了数学机械化证明的历史及国内外研究现状,其次介绍了Mizar系统的发展历程和研究。基于数学定理的机器证明和数学定理自动推理系统Mizar,对一些特殊函数类积分问题和数论中的简化剩余系问题进行了Mizar表述和推证,且通过了Mizar系统验证。主要研究成果和创新点如下:1.在Mizar系统下给出了特殊函数积分公式的表述与论证,其中包括有理数函数,无理数函数,三角函数,反三角函数,指数函数,对数函数,复合函数的Mizar表述与实现;2.基于Mizar系统定义了以第一类间断点为瑕点的广义积分,并在此基础上给出了积分区间端点同时为瑕点的瑕积分的Mizar定义表述及证明,论证了瑕积分的某些性质;3.定义了简化剩余系并证明了其部分性质;4.讨论了指数的某些性质,并结合简化剩余系的定义和性质给出了原根的定义,从而根据两者的关系阐述了简化剩余系的几何级数的表示形式。以上结果都通过了Mizar系统的验证,其中前一部分被收录于最新的Mizar数学数据库MML中,并发表于2010年的Formalized Mathematics期刊。