基于Coq的不用极限微积分形式化验证

rtificial intelligence is one of China's current major science and technology development strategies. Mathematical formalization, as an important theoretical basis for artificial intelligence, is of great significance to the development of science and technology. Based on the proof assistant Coq, this paper realizes the formal verification of calculus without limit theory, includes Coq descriptions of Uniformly Continuity, Uniformly Derivable, Strongly Derivable and Integral System. Then, this paper prove some properties of Uniformly Derivable and Valuation Theorem with Coq, all formalization processes have been verified by Coq. The formalization demonstrates that the Coq-based mechanized proof of mathematics theorem has the characteristics of readability and interactivity.