An Interactive Algebra Course with Formalised Proofs and Definitions

Abstract. We describe a case-study of the application of web-technology (Helm [2]) to create web-based didactic material out of a repository of formal mathematics (C-CoRN [5]), using the structure of an existing course (IDA [4]). The paper discusses the difficulties related to associating notation to a formula, the embedding of formal notions into a document (the "view"), and the rendering of proofs.4 1 Introduction One of the aims of the recently concluded European IST Project MoWGLI wasthe development of a suitable technology supporting the creation of web-based didactic material out of repositories of formal mathematical knowledge. In particular, the validation activity reported in this paper consists of theapplication of the Helm [2] technology, developed at the University of Bologna