本书利用交互式定理证明工具Coq，在朴素集合论和初等数论及代数知识形式化系统下，以华东师范大学数学系编著的《数学分析》为基本构架，实现一元微积分的机器证明系统，包括实数与函数、数列极限、函数极限、函数的连续性、导数和微分、微分中值定理、实数的完备性、不定积分、定积分以及两个重要极限等内容的形式化实现。

更多科学出版社服务，请扫码获取。