Formalization Of The Basic Framework Of Ring And Field Theory Based On Coq

As an important driving force for a new round of technological revolution and industrial change,artificial intelligence is a strategic technology that leads the future and has officially risen to the national strategy.A very important branch of artificial intelligence is automatic reasoning.A lot of work on automatic reasoning is focused on theorem machine proof.Theorem machine proof refers to the use of a computer to prove the establishment of the theorem,that is,the process of human proof of the theorem is formalized through a set of symbolic systems,and becomes a series of symbolic calculation processes automatically implemented on computers.It is the main attack of modern artificial intelligence.One of the topics.Coq is an interactive theorem proof tool based on inductive construction calculus.It uses types to describe and prove programs or propositions that need to be verified,which is very suitable for programs that need to strictly conform to specifications.At present,in the field of theorem machine proof at home and abroad,Coq is one of the mainstream auxiliary proof tools.It has a strong mathematical model foundation and good extensibility,and has a complete tool set.In reasoning and programming,Shows strong expression skills.Order structure,algebraic structure,and topological structure are the three basic mother structures of mathematics.The fusion of these three mother structures promotes the deep development of mathematics.Algebraic structures include groups,rings,and domains.Among them,groups are the basis of rings and domains.Groups have a pivotal position in the field of mathematics,and they are also widely used in other disciplines.The machine proof of the mathematical theorem is the embodiment of mathematical reliability and rigor.The theorem verified by the machine is completely credible,and it connects the computer field and the mathematical field.Formalizing group theory is the process of verifying it,and it has profound significance in the field of machine proof of mathematical theorems.Based on the book "Modern Algebra" by Professor Zhang Herui as the theoretical basis,this paper builds a formal system of group theory based on the interactive theorem proof tool Coq.Starting from the basic concepts of modern algebra,this paper gives formal definitions of concepts such as sets,mappings,algebraic operations,and relations.Then,operations are added to sets to define the concept of groups.Then we discuss some special groups and define subgroups.Based on the invariant subgroups,we discuss the Homomorphism of group,invariant subgroups and quotient groups.Finally,we give formal proofs for some important theorems in group theory.The innovation of this article is to use Coq to achieve the formal description of the above definition and the rigorous proof of the theorem.The formalization of group theory not only verifies the rigor and reliability of the group theory system,but also a successful mathematics in the field of artificial intelligence.