A Machine Proof System Of The Third Generation Calculus In Coq

The research of artificial intelligence is the hot spot and forward direction of current science and technology development.It is especially important to tamp down the basic theory of artificial intelligence.The mechanical proof of mathematical theorem is the profound embodiment of the basic theory of artificial intelligence.Mechanical proof of theorems mainly refers to the realization of mechanical proof of mathematical theorems by means of computer technology,thus realizing the mechanization of mental work in mathematical reasoning.In recent years,with the development of computer technology,especially the emergence of some auxiliary tools for theorem proving such as Coq,Isabella,HOL Light,the research of mathematical theorem machine proving has made great progress.For the formalization of mathematical theory,the mechanization of calculus is more fundamental.Calculus is one of the greatest achievements in the history of mathematics.It not only opens a new era in the development of mathematics,but also plays an important role in promoting the development of human science and technology.However,the complex concept of limit in traditional calculus has raised the threshold for learning calculus.Therefore,scholars at home and abroad have been devoted to the research of new generation calculus and have achieved certain results.Based on the proof assistant Coq,this paper realizes the formal verification of the theoretical framework of the third generation calculus-calculus without limit—advocated by Academician Lin Qun and Academician Zhang Jingzhong.The main work includes:1.Based on the definition of real numbers in Coq library,this paper gives the formal description of basic definitions such as set,interval,function,etc.,which makes necessary preparations for building the theoretical framework of calculus.2.In strict accordance with the article entitled "A New Perspective of Calculus Foundation" published by Zhang Jingzhong et al.,this paper realizes the formal description of uniform continuity,uniform(strongly)derivable,integral system,integral strict inequality and valuation theorem.3.On the basis of the definitions of derivative and integral without limit concept,this paper realizes the formal verification of the basic theorem of calculus,including:the relation theorem between monotonicity of function and derivative,Newton-Leibniz formula,differentiability of variable upper limit integral Taylor formula.In this paper,all formalization processes have been verified by Coq and run thought on the computer.The formal proof demonstrates that the Coq-based mechanized proof of mathematics theorem has the characteristics of readability and interactivity.The proof process is standardized,rigorous and reliable.This paper is an attempt of the idea that researchers learn,understand,construct,educate and even develop mathematical theories with computer.