| 摘要: |
| 形式化数学是一次数学革命, 结合定理证明器的数学定理机器证明, 不仅是对数学严谨性的一种新标准, 更是发展数学的一种新方式. 随着世界范围不断有数学难题在计算机辅助下的成功解决, 以及专家学者对各种数学形式化项目或工程的发起, 形式化数学的影响力与日俱增, 在数学界与计算机界引起广泛影响. 介绍一项基于定理证明工具Coq的数学分析形式化系统, 该系统以华东师范大学数学系编著的《数学分析》为蓝本, 在朴素集合论和初等数论及代数知识体系下进行开发. 当前, 已经实现其上册中一元微积分相关内容的形式化, 包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、不定积分、定积分等内容. 该系统严格对应教材内容, 全部定理无例外地给出Coq的机器证明代码, 所有形式化过程已被Coq验证, 并在计算机上运行通过. 读者可以跟随代码学习数学, 也能够对照数学理解代码, 充分体现了基于Coq的数学定理机器证明具有可读性、交互性和智能性的特点, 实现让读者跟随计算机学习、理解、构建、教育乃至发展现代数学的尝试, 提高认识数学、感受数学和欣赏数学的素养. |
| 关键词: 形式化数学 定理机器证明 Coq 数学分析 一元微积分 |
| DOI：10.13328/j.cnki.jos.007604 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金(62476028) |
|
| Mechanizing Mathematical Analysis I: Formal System of Single-variable Calculus |
|
DOU Guo-Wei1,2, YU Wen-Sheng1,2
|
|
1.School of Electronic Engineering, Beijing University of Posts and Telecommunications, Beijing 100876, China;2.Beijing Key Laboratory of Space-ground Interconnection and Convergence, Beijing University of Posts and Telecommunications, Beijing 100876, China
|
| Abstract: |
| Formalized mathematics represents a revolution in mathematics. The combination of theorem provers with machine verification of mathematical theorems establishes not only a new standard for mathematical rigor but also a novel approach to developing mathematics. As mathematical challenges worldwide are increasingly solved with computer assistance and various formalization projects are launched by experts, the influence of formalized mathematics continues to grow. It generated significant impact across both the mathematical and computer science communities. This study introduces a formal system for mathematical analysis based on the Coq theorem prover. The formalization is guided by the textbook Mathematical Analysis compiled by the School of Mathematical Sciences at East China Normal University. Developed within the framework of naive set theory and elementary number theory and algebra, the system has formalized the content related to single-variable calculus from the first volume of the textbook. It includes topics such as real numbers and functions, sequence limits, function limits, continuity of functions, derivatives and differentials, indefinite integrals, and definite integrals. The proposed system strictly corresponds to the textbook content, where all theorems are provided with machine-verifiable Coq proofs. The entire formalization is verified by Coq and executed successfully on a computer. Readers can learn mathematics by following the code and can also understand the code by comparing it with the mathematics, which demonstrates the readability, interactivity, and intelligence of Coq-based machine theorem proving. It represents an attempt to enable readers to follow the computer in learning, understanding, constructing, educating, and even developing modern mathematics, thereby enhancing their ability to understand, experience, and appreciate mathematics. |
| Key words: formalized mathematics machine-assisted theorem proving Coq mathematical analysis single-variable calculus |
