论文标题
AGDA证明助手的建设性分析
Constructive Analysis in the Agda Proof Assistant
论文作者
论文摘要
证明助理软件最近已被用来验证主要定理的证明，但即使是一些最杰出的证明助手的图书馆也缺乏大量的本科数学。特别是，AGDA证明助手对实际数字及其算术没有形式化。在这篇论文中，我介绍了埃雷特·毕晓普（Errett Bishop）在AGDA中的建设性实数的实施，包括它们的算术，订购和基本结果，例如非成绩和库奇完整性。我们还将调查建设性分析和AGDA证明助手的基本概念。
Proof assistant software has recently been used to verify proofs of major theorems, yet even the libraries of some of the most prominent proof assistants lack much of undergraduate mathematics. In particular, the Agda proof assistant has no formalization of the real numbers and their arithmetic. In this thesis, I present my implementation of Errett Bishop's constructive real numbers in Agda, including their arithmetic, ordering, and fundamental results, such as uncountability and Cauchy completeness. We will also survey the basic concepts of constructive analysis and the Agda proof assistant.
