数学问题的机器证明是利用计算机证明和求解数学问题。Mizar语言系统是上世纪八十年代开创的集逻辑证明、校验、排版功能于一体的计算机语言系统。如今该系统已拥有自身的数据库MML，收录了几乎涵盖数学各个分支的1000多篇数学论文。同时，Mizar语言系统在自动化控制、声音和图像识别等研究领域也有着广泛的应用。 本文首先介绍了定理机器证明和Mizar语言系统的发展历史，其次简单描述了Mizar系统下定理机器证明和校验数学命题的方法，在此基础上对四元数的混合运算，特殊复合函数的微分以及罗尔定理的应用等方面进行了Mizar实现。 本文主要工作： 1．在Mizar系统中定义了有关四元数的几个概念，完成了四元数的混合运算性质的Mizar实现，对于四元数模的一些相关命题也进行了一定的Mizar论证。 2．基于Mizar数据库中已有的三角函数、幂函数、对数函数及可微性定理，成功地对一些特殊复合函数的微分进行了Mizar实现。 3．将Mizar系统中已实现的罗尔定理与相关数学知识相结合，在Mizar系统中实现了罗尔定理和柯西中值定理的一些应用和推广。 以上结果均已通过Mizar语言系统的验证，部分内容已被收录在Mizar数据库MML中。