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
possibility?
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