1. Web-based input of definitions and theorem statements
No due date
60% complete
This is the bare minimum that is required for others to meaningfully contribute to the library.
Incorporates both the input via the GUI and the necessary type checking, but no proof input. Most of this has already been implemented in the desktop version.