A Real Semantic Web for Mathematics Deserves a Real Semantics

Abstract. 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 [2] support the first two of these, with little, if any, contribution to the third, while Proof Assistants [17] 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 "MathWiki" to harness Web 2.0 tools and techniques to the rich semantics furnished by contemporary Proof Assistants. 1 Background and state of the art We can identify four worlds of mathematical discourse available on the Web:

• Type: Conference
• Year: 2008
• Where: SEMWIKI
• Authors: Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
• Keywords: Data Mining, Mathematical Documents, Proof Assistants, Semantic, SEMWIKI 2008