A computer system with the preliminary name “Logiweb” will be presented. Logiweb is a web-like system that allows logicians to web-publish papers with high typographic quality. Among other, Logiweb allows papers to contain definitions of formal theories, definitions of new constructs, programs, lemmas, conjectures and proofs. Furthermore, Logiweb allows papers to refer to each other, and allows proof checking of proofs that span several papers. As an example, a lemma in one paper may refer to a construct which is defined in another paper, in which case the proof checker must access both papers to establish the correctness of the proof.
Logiweb is going to be used by first year students and by graduate students at the University of Copenhagen this fall. For the graduate students, the intension is that the definitions of Peano arithmetic and ZFC are put on web, and that all lemmas from a textbook in logic are placed on the web as conjectures. It will then be up to the students to prove conjectures from previous conjectures in any, random, order. When each conjecture is proved by at least one student, all the conjectures will then turn into lemmas.
The talk will present Logiweb and some of the problems such a system must tackle (e.g. that no two mathematicians use the same notation, but still refer to the papers of each other). A very preliminary version of the Logiweb system will be available for hands on experience.