计算机证明数学问题是当今世界积极研究的一个热门领域。迄今为止，世界已有多种可用来进行数学命题证明和逻辑推理的机器语言系统，但其中只有少数几种语言可被普遍接受并受到数学家与计算机专家的认可，如HOL、Mizar、PVS、Coq等，它们各自的初衷不同，却有一个共同的特征：人类使用机器语言书写、计算、逻辑推理和证明文本性质的数学问题，并由计算机自动验证其正确性。这里讨论的Mizar系统是由波兰Hock科学协会的Andrzej Trybulec教授领导下开发的。经过近30年的发展，Mizar系统已经形成了著名的数学知识处理的形式化系统。在此系统下，完成了大量的数学问题的计算机证明。这些数学知识涵盖了几乎数学的每一个分支，解决了人们用手无法计算和证明的一些复杂问题。同时，它在自动控制、声音和图像识别等研究领域有着广泛的应用，为今后讨论数学及其相关学科奠定了一个良好的基础。 本文首先介绍了Miear系统的计算机操作原理和使用方法，给出了在Mizar语言系统下四元数、四元数的运算、共轭、内积、模等代数结构理论的证明，所做结论都通过了Mizar系统的验证，发表在波兰的《Formalized MalIhematics》杂志上，并被收录到MML数据库中。