What's in the Math Library?

The library has been around for four years, and i think it's interesting to note that it knows about as much as an undergraduate would know if they'd spent four years in school. But of course, let me stress, it's not thinking in the same way as a human, right? It's checking results which humans are typing in, right? You give it a question, it'll say, yes, ok. And i understand the statement of the question. But you ask an undergraduate to solve the question, and the undergrads might start having ideas. Whereas right now, lean just says, well, you know, i'd be very happy if you were to type in a