当前，数学问题计算机证明的研究已成为世界各国积极研究的前沿领域。随着计算机技术的发展，人们己根据机械化方法创建了各种机器语言来编写程序，在计算机上给出相应数学问题的机器证明。　　 本文介绍了数学问题计算机证明的Mizar语言系统，应用Mizar语言系统对有限群不同问题给出了相应的证明，主要工作如下：　　 1.在某种意义下将群的子群与群的同余关系同等看待，在Mizar语言系统下定义了群的子集关于子群的上、下近似，证明了粗糙子集的若干性质；　　 2.应用群的正规子群与群的同余关系一一对应关系，在Mizar语言系统下得出群的子群关于正规子群的上、下近似并进一步得到群的粗糙子群的理论：　　 3.给出了幂零群Mizar语言系统下的定义，证明了幂零群的若干性质和幂零群的充要条件；　　 4.给出了若干幂零群的充分条件，指明了幂零群与可解群的关系；　　 5.给出了р-元素Mizar语言系统下的定义，证明了р-群的等价定义，讨论了р-群的若干性质；　　 6.在р-群的基础上给出了р-交换群的定义，证明了р-交换群的若干性质。　　 以上结果已经通过Mizar语言系统的验证，相关内容已经在Formalized Mathematics发表。