Constructive Analysis in the Agda Proof Assistant

TL;DR

This paper presents a formalization of Errett Bishop's constructive real numbers in Agda, including their properties and fundamental theorems, filling a gap in the mathematical libraries of proof assistants.

Contribution

The paper introduces the first comprehensive formalization of constructive real numbers in Agda, including their arithmetic, ordering, and key properties like uncountability and completeness.

Findings

Formalization of constructive real numbers in Agda

Proof of uncountability and Cauchy completeness within Agda

Survey of constructive analysis concepts

Abstract

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.