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.},\n}\n'