数学机械化是数学与计算机科学相结合的一个新学科，随着数学研究及计算机科学的发展，它已经成为非常活跃的研究领域。为了实现数学机械化，各种计算机语言应运而生。Mizar系统语言便是其中之一。Mizar系统是用于证明和求解数学问题的计算机语言系统。目前Mizar系统拥有世界上最大的数学数据库（MML），至今已经收录了千余篇文章，四十余万条定理，几乎涵盖了数学领域的所有分支。　　本文首先介绍了数学机械化及Mizar系统的发展历史，其次对如何利用Mizar语言撰写数学论文和进行自动推理校验给出了简要的说明。本文主要研究了Euler函数性质及有限序列乘幂的定义在Mizar系统下的实现，并在此基础上，实现了它们的性质定理的证明。本文研究成果及创新点如下:　　1给出了其他一些定义模式下Euler函数的定义及简单性质，并给出了相应的证明;　　2在Mizar系统下，首次给出了有限序列乘幂的定义，并完成了相应的运算公式及定理的Mizar证明。特别的，在此基础上完成了算术基本定理在Mizar系统下的证明;　　3将有限序列乘幂的理论应用到Euler函数的研究中，由此在Mizar系统下第一次给出了任意非零自然数的Euler函数表达式以及各非零自然数的Euler函数之间的关系。证明了Euler函数值域包含在偶数域中，并讨论了Euler函数与素数的关系。