An automated, searchable, fully relational store of topological information.
Suppose you are interested in a property P and have shown that Perfectly Normal ⇒ P, CCC ⇒ P, and P ⇒ Completely Regular. Here, you simply add those theorems, let the site deduce what it can about the spaces it knows, and then search for spaces where P is still indeterminate. This streamlines time-consuming literature study and allows researchers to benefit from pooling their knowledge of exotic examples.
Every piece of information in the database should be traceable back to first principles, so students can search for an interesting example and then follow along with deriving its properties. Admittedly, there are currently several traits missing proofs - consider those your homework assignment.