人工智能是作为新一轮科技革命和产业变革的重要驱动力,是引领未来的战略性技术,已正式上升为国家战略。而人工智能中一个非常重要分支就是自动推理,自动推理的大量工作都集中在定理机器证明中。定理机器证明是指使用计算机证明定理的成立,即把人证明定理的过程,通过一套符号体系加以形式化,变成一系列在计算机上自动实现的符号计算的过程[1],它是人工智能近代主攻的课题之一。Coq是一个基于归纳构造演算的交互式定理证明工具[2],它使用类型对需要验证的程序或命题进行描述和证明,非常适合证明需要严格符合规范的程序。目前,在国内外的定理机器证明领域,Coq是主流的辅助证明工具之一,它有着强大的数学模型基础和良好的扩展性,并拥有完整的工具集[3],在推理和编程方面,表现出强大的表达能力。序结构、代数结构、拓扑结构是数学的三大基本母结构,这三大母结构的交融促进了数学的纵深发展。代数结构包括群、环、域三大结构[4-6],其中群是环和域的基础,群在数学领域有着举足轻重的地位,在其他学科也有广泛的应用。数学定理的机器证明是数学可靠性和严谨性的体现,它连通了计算机领域和数学领域,通过机器验证过的定理是完全可信的。对群论实现形式化是对其进行验证的过程,在数学定理的机器证明领域具有深刻意义。本文以张禾瑞教授的著作《近世代数基础》作为理论依据,基于交互式定理证明工具Coq,构建了群论体系的形式化系统。本文从近世代数的基本概念出发,给出了集合、映射、代数运算、关系等概念的形式化定义,然后给集合加上运算,定义出群的概念。接着讨论了一些特殊的群,并定义出子群,在不变子群的基础上讨论了群的同态、不变子群和商群,最后针对群论中的一些重要定理给出了形式化证明。本文的创新点在于利用Coq实现了以上定义的形式化描述以及定理的严谨证明,群论的形式化不仅验证了群论体系的严谨性与可靠性,更是数学在人工智能领域的一个成功的案例。