Machine Proof Of Newton-Leibniz Formula Based On Coq

As the times growing quickly,the progress of computer technology is like a broken bamboo,artificial intelligence(AI)is a case in point.Machine theory proves to be a significant content of AI,and its origin can be traced back to the Leibniz era,involving multiple disciplines such as computers,mathematics,and so on.The genesis of machine theorem demonstrating may be retraced to the Leibniz times,It is an interdisciplinary subject of mathematics,logic and computer science.The automatic theorem evidencing technology purposes to implement the automatic proof of the computer.As time goes by,the interactive proof tool,also known as the proof assistant,came into being.Coq is an international mainstream interactive proof tool that relies on its rigor,robustness,credibility and other characteristics.It is based on the computer language Gallina,legal naming and code specifications to achieve mathematical theorem proofs or system security verification.Through human-computer interaction,the computer assists people to complete the inference process of mathematical theorems.The formal research of mathematical theorems is of great significance.It can not only promote the development of formal mathematics,but also help readers have a deeper understanding of mathematical theorems.The emergence of calculus has made great contributions to modern science,and played an important role such as mathematics,physics and so on.Understanding the Newton-Leibniz formula is of great significance to the establishment of the calculus system.This dissertation will be relied on"mathematical analysis",and the book was completed by the academy of Mathematics of ECNU,The mathematical theorems in the calculus system will be formalized.The Newton-Leibnitz formula establishes a link between the division and the integral.Based on the interactive proof tool Coq,starting from the prerequisite knowledge in the construction system—sets and functions,this paper first completes the formal proof of the basic content of calculus.This part describes the real numbers,sequence limits,function limits and continuous functions one by one,and then on the foundation of the realization of the derivativation,the theorem of Lagrange,and the integration,The formalization of the Newton-Leibnitz formula is finally accomplished.