Formalization Of Advanced Algebra In The View Of Modern Algebra

Artificial intelligence is an important branch of the computer sicience discipline.Together with genetic engineering and nanoscience,they are considered to be the three cutting-edge technologies of 21th century.With the rapid development of artificial intelligence,the reliability of its basic theory is particularly important.One of the basic theories of artificial intelligence is the machine proof of the mathematical theorem.The interactive theorem-proving tool Coq is a powerful tool for the proof of mathematical theorems.Coq can not only be used to verify the accuracy of logic in ordinary mathematics,but also to strictly verify procedures or theories.In addition to a strong mathematical model foundation,Coq has good scalability,and the complete tool set makes it easier to use.Formalization is flourishing with the development of modern mathematics,and the interactive theorem-proving tool Coq has also achieved many outstanding achievements along with the development process.The reliability of the proof of the mathematical theorem is the embodiment of the rigor of the basic theory of mathematics.The three maternal structures(order,algebra,topology)of the Bourbaki,as the basis of modern mathematics,play a pivotal role in the history of mathematics.Due to the universality of algebraic elements,algebraic structures have been used as the basic tools and language for their research in many fields.Algebraic systems,also seen as sets with operations,are the basic objects of algebra research.Modern algebra is a discipline that studies algebraic systems.Groups,ring,and domains are the most basic three algebraic structures.Under the guidance of the ideas of the algebraic infrastructure,this paper systematically summarize and enhances the content of advanced algebra.Using the interactive theorem-proving tool Coq,we can construct a formal system of modern algebra theory,so that advanced algebra systems under the concept of modern algebra can also be established naturally.Starting from the most basic modern algebra theory,this paper first establishes the basic concepts of group,ring and domain.On the basis,the concepts of vector space and linear transformation in advanced algebra are established.Based on the basic theory of modern algebra,the isomorphism theorem of vector space and the Rank-nullity theorem are formalized and elaborated.All formalization procession have been verified by Coq,reflecting the efficiency,readability and rigor of it.