My feeling about this is closest to the answer by Timothy Chow. First somewhere I can look up a definition or a named theorem would be better off somewhere else. There are existing databases that have proved themselves useful. The OEIS is far more useful than I would ever have expected. John Cremona's database of elliptic curves is the result of a lifetime's hard work although I have not used it myself. Again it is not my field but my understanding is that GAP includes many databases that have been built up over years. There is also Thistlewaite's KnotScape and Bar Natan's KnotAtlas which are databases of knot tables and knot invariants. There is also Nauty which produces great lists of graphs and related stuctures.
It seems to me that all of these become far more useful if the database is part of a computer algebra package. Furthermore that it is not just the data but the calculations that can be done with it that make it useful to mathematicians.
My feeling is that 5. 6. 7. are covered already in computer algebra packages.
Edit: Of course I left out the two databases that I use without thought. MathSciNet and the arXiv.
