Mizar系统是用于证明或计算数学问题的计算机语言系统。它由波兰华沙大学AndrzejTrybulec教授组织的Mizar协会领导，其逻辑框架是基于Jaskowski自然演绎推理的古典逻辑。Mizar如今已经成为集自然演绎、逻辑证明、复杂计算、验证排版、科研教学于一体的处理数学知识的形式化系统，拥有自己的数据库MML，其中收录了几乎涵盖数学各个分支的上千篇论文。尤其在证明不同维数的Jordan曲线定理、集值映射的不同点定理和代数与拓扑结构方面的部分重要定理等诸多方面突显出Mizar语言系统的优越性。 本文首先介绍了Mizar系统的历史和研究现状，对如何利用Mizai语言完成数学论文和进行自动推理验证给出了简要说明。作者在Mizar系统下推导出一次同余式和一次同余式组的求解公式、证明了平方剩余和Legendre符号的一些性质及原根指数的相关定理，并针对不同的数学问题给出了相应的算法和证明方法，且通过了系统验证。作者的主要工作如下： 1、实现了完全剩余系和同余关系的Mizar表述及其定理证明；推导出一次同余式和一次同余式组的求解公式，并给出了相应的证明方法。 2、定义了整系数多项式、平方剩余和Legendre符号，讨论了它们之间的相互关系，并验证其正确性。特别地，利用反证法和数学归纳法实现了Gauss引理和二次互反律的证明。 3、进一步讨论了指数的一些性质；实现了简化剩余系的Mizar表述和重要性质的证明，在此基础上，给出了原根的Mizar表述及其几何级数形式和相关定理的证明。 以上结果都通过了Mizar系统的验证，其中前两部分被收录于最新的Mizar数据库MML中，分别发表于2007和2008年的FormalizedMathematics期刊。