The existence of extensive libraries of formal mathematics in the system opens the possibility that interested students will explore on their own. For example, there is a proof of the FTA in the algebra library done for unique factorization domains. The account is a direct generalization of the results in the number theory library, so a student might learn about abstract algebra just by following leads.
We expect that students will contribute to the courseware not only by adding solutions to exercises, but from time to time, by creating new sub-libraries of material that interests them. Having this chance to create new formal mathematics or new algorithms might be an exciting outlet for budding scientists.