Mathematical documents, and their instrumentation by computers, have rich structure at the layers of presentation, metadata and semantics, as objects in a system for formal mathematical logic. Semantic Web tools  support the first two of these, with little, if any, contribution to the third, while Proof Assistants  instrument the third layer, typically with bespoke approaches to the first two. Our position is that a web of mathematical documents, definitions and proofs should be given a fully-fledged semantics in terms of the third layer. We propose a "Math- Wiki" to harness Web 2.0 tools and techniques to the rich semantics furnished by contemporary Proof Assistants.
ASJC Scopus subject areas
- Computer Science(all)