# Item

ITEM ACTIONSEXPORT

Released

Thesis

#### Towards a Natural Representation of Mathematics in Proof Assistants

##### MPS-Authors

##### Locator

There are no locators available

##### Fulltext (public)

There are no public fulltexts available

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Horazal, F. (2007). Towards a Natural Representation of Mathematics in Proof Assistants. Master Thesis, Universität des Saarlandes, Saarbrücken.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0027-CF7A-B

##### Abstract

In this thesis we investigate the proof assistant Scunak in order to explore
the relationship between informal mathematical texts and their Scunak
counterparts. The investigation is based on a case study in which we have
formalized parts of an introductory book on real analysis. Based on this case
study, we illustrate significant aspects of the formal representation of
mathematics in Scunak. In particular, we present the formal proof of the
example lim(1/n) = 0.
Moreover, we present a comparison of Scunak with two well-known systems for
formalizing mathematics, the Mizar System and Isabelle/HOL. We have proved the
example lim(1/n) = 0 in Mizar and Isabelle/HOL as well and we relate certain
features of formal mathematics in Mizar and Isabelle/HOL to corresponding
features of the Scunak type theory in light of this example.