** Next:** Introduction

# Formalizing Constructive Real Analysis

** *** Max B. Forester*

* Department of Computer Science*

* Cornell University*

* forester@cs.cornell.edu*

**July 16, 1993**

### Abstract:

*This paper arises from a project with the Nuprl Proof Development System which
involved formalizing parts of real analysis, up through the intermediate value
theorem. Extensive development of the rational library was required as the
real library was being built, resulting in the addition of about 125 rational
theorems. The real library now contains about 150 theorems and includes enough
basic results that further extensions of the library should be quite feasible.
This paper aims to illustrate how higher mathematics can be implemented in a
system like Nuprl, and also to introduce system users to the library.
*