Re: Examples

F. Javier Thayer (
Sat, 18 Jun 1994 10:09:59 -0400

>> Could you suggest something?

I'm not sure what the question is, but I assume you want me to
suggest something that is possible to do from the existing Mizar
library of theorems. Wouldn't a development of the first few chapters
of Dieudonne's book "Foundations of Modern Analysis be" a

I also think Victor Yodaiken's suggestion of "Concrete Mathematics"
is an ambitious, but in my opinion feasible project using any of the
currently existing theorem checkers/provers. THAT would be real eye
catcher don't you think?

Javier Thayer