Type theory offers a lot of structure to allow indexing schemes for
theorems and to provide hints and cues for applicability of these
known theorems. For instance, IMPS uses these cues extensively in its
macete lookup mechanism.
Unfortunately, much of mathematics is hard to encase within a fixed
type system. For instance, most of topology or geometry cannot be
considered the study of a single toplogical or geometric object. In
fact, it is frequently the case that one considers whole families of
the these objects. I don't know how to treat these within a simple
type theory without fundamentally cheating (that is, without
establishing some imbedding of them in set theory.) This problem is
especially annoying if one is to handle in a conventional way any of
the structure theorems of basic mathematics, such as the structure
theorem for finitely generated abelian groups.