Title:machine Proof System Of Linear Algebra In The View Of "Module" Based On Coq

In recent years,artificial intelligence has developed rapidly and has risen to a major national strategy.It is particularly important to consolidate the basic theory of artificial intelligence.The machine proof of mathematical theorem is a profound manifestation of the basic theoretical research of artificial intelligence,and is the perfect combination of computer science and mathematics.It mainly uses computer to formally describe mathematical theory and verify the correctness of theorem proof.With the advent of proof auxiliary tools such as Coq,Isabella,HOL Light,the machine proof of the theorem has made great progress.According to the Burbaki group from France,modern mathematics consists of three structures:order structure,algebra structure and topology structure.Linear algebra occupies the first place in all kinds of branches of algebra.It is one-sided to discuss only the structural properties of vector space in linear algebra,but also to consider the role of linear transformation in it,which is the originality of the module view.Using the module theory of modern algebra to study linear algebra makes linear algebra from classical to modern.The vector space with linear transformation can be seen as a module on the principal ideal domain.Therefore,the module decomposition theorem plays an important role in the decomposition of vector space.Based on the Coq proof assistant,starting from the research achievement of our laboratory-formal system of axiomatic set theory,this paper preliminarily realizes the formalization of linear algebra system from the perspective of module,and on this basis,completes the machine proof of module decomposition theorem.The main research contents of this paper are as follows:1.Using Coq,based on the formal system of axiomatic set theory and Sheng Gong’s "five lectures on linear algebra",formalize constructed algebraic structures such as group,ring,division ring,field and principal ideal domain,and complete the machine proof of the decomposition theorem of prime element on the principal ideal domain.2.The two algebraic structures of vector space and module are formalized,and the main relations and differences between them are explained in code.So far,a formal framework of algebraic structures has been established.3.The machine proof of the decomposition theorem of finitely generated module on the principal ideal domain is completed,including the machine proof of the decomposition theorem of finitely generated module,the machine proof of the unique decomposition theorem of quasi prime and the machine proof of the uniqueness theorem of cyclic decomposition.This theorem can be regarded as a bridge between vector space and module,which is of great significance to the follow-up formal study of linear algebra.All formal processes in this paper have been verified by Coq,which reflects the reliability and rigorous characteristics of Coq-based mathematical theorem machine proof,and the process is standardized,readable,and intelligent.