I'm contemplating two projects for final-year CS students to do: 1) Thinking of mathematics as (partly comprising) a set of: Theorems with Preconditions and Proof(s), Generalisation theorem-theorem relationships, Theorem-(used in/by)-Proof relationships Counterexamples ... I see this information forming a database with an application 'projecting' this information to a web-interface which allows one to navigate around 'theorem space'. This seems well-suited to the web, and the opportunities of multimedia (graphics, animation, video, sound) is just a bonus - perhaps helped also by the XML-style language MathML. I'm thinking of asking a CS student to create such a system. Question is - is there anything out there of this kind already? 2) The intended system is a 'Logic Assistant'. A user-student would be trying to prove something using the formal means of a logic with already-known results and rules of inference. The system would either know the proof (as provided data) or be trying to work it out too [and I think there are systems for this 'out there' but I don't know about them]. The student would start with say 100 points and lose a few points for every 'atom' of hint provided by the system. The system would be able to manage hints, compare what the student proposed with the right answer, and general be an assistant/mentor/tutor in the learning process. Same question as for '1' really - is there anything out there of this kind already? Thanks in advance for any inputs - Guy Haworth, Univ of Reading, UK