Formal Representation of Mathematics in a Dependently Typed Set Theory

Abstract. 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.

• Type: Conference
• Year: 2007
• Where: MKM
• Authors: Feryal Fulya Horozal, Chad E. Brown
• Keywords: Dependent Type Theory, Formalized Material, MKM 2007, Proof Assistant Scunak