Formal Representation of Mathematics in a Dependently Typed Set Theory.

We have formalized material from an introductory real analysis textbook in the proof assistant Scunak. Scunak is a system based on set theory encoded in a dependent type theory. We use the formalized material to illustrate some interesting aspects of the relationship between informal presentations of mathematics and their formal representation. We focus especially on a representative example proved using the system. [ABSTRACT FROM AUTHOR]