基于Coq的多项式理论形式化

s an important driving force of a new round of scientific and technological revolution, artificial intelligence research is a hot spot in the development of science and technology. As an important branch of artificial intelligence, theorem machine proving is a perfect combination of computer science and mathematics.Algebraic system is a basic subject of mathematics, which has become an auxiliary tool in many fields such as physics and computer science.This paper realizes the formalization of polynomial theory based on the interactive theorem proof assistant tool Coq. For two systems of integer and polynomial, it defines its four operations, realizes the Coq description of related theorems such as divisibility and maximum common factor. All theorems give the Coq formal proof code without exception, and run on the computer through it.The description of the definition and the proof of the theorem are clear, accurate, precise and reliable, which fully reflects the features of Coq readability, intelligence and reliability.This paper is widely used, which has laid a solid foundation for the follow-up study of determinant, vector space and other mathematical structures. The results can also be used in computer-aided design, cryptography and other related fields.