在新一轮的技术变革中,人工智能是十分关键的推动因素,是当前科技发展的热点内容,该领域的重要分支之一就是定理机器证明,充分的融合了计算机和数学这两大专业科目。近年来,形式化方法在数学领域更加受到重视,主要用于研究数学定理的形式化证明,不同于传统依据直觉进行判断的人工证明,形式化证明的每一个步骤都严谨可信。随着计算机科学和形式化证明的迅猛发展,出现的证明辅助工具Coq完成了多项著名定理的证明,成为形式化证明的得力工具。代数系统是数学基础性学科,已成为物理及计算机科学等多个领域的辅助性工具。代数学从基础不断拓展至更深入的研究所得到学科的统称即为高等代数,其中包括多项式理论。多项式是一类应用广泛的常见函数,是代数论基础的研究对象。本文以张禾瑞先生的《高等代数》教材为理论依据,基于交互式定理证明辅助工具Coq,实现多项式理论的形式化。证明系统以数学基础的集合和映射为起点,对重要的数学证明方法——数学归纳法完成Coq证明,针对整数部分的带余除法、最大公因数等定义进行描述,相关性质实现Coq证明;由数到式,完成多项式系统的定义,实现多项式中带余除法定理、最大公因式的定理描述和证明,引入互素的概念并证明其相关性质。本文全部定理无例外的给出Coq形式化证明代码,在计算机上运行通过。定义的描述与定理的证明过程清晰准确、严谨可靠,充分体现了 Coq可读性、智能性与可信性的特点。本文为后续研究代数学其他数学结构奠定了坚实的基础。