From MathWeb

Rationale for a “mathematical semantic web“:

Mathematicians need semantic-web-like services that solve problems like the following (quoted from the OMDoc book):

• Cut and paste on the level of computation (take the output from a web search engine and paste it into a computer algebra system),
• Automatically proof checking published proofs,
• Math explanation (e.g. specializing a proof to an example that simplifies the proof in this special case),
• Semantic search for mathematical concepts (rather than keywords),
• Data mining for representation theorems (are there unnoticed groups out there?),
• Classification: Given a concrete mathematical structure, is there a general theory for it?

The current semantic web, on the other hand, had different origins: first, annotating content with metadata like Dublin Core, then doing the next step towards RDF (for more annotation than just metadata), then formalizing the vocabularies using ontologies, e.g. given in description logic. Many services based on these concepts are available, but only a few are suitable for mathematical applications.

Mathematicians do not care about metadata and annotations, they start thinking formally, but not in classes and properties (as DL does), but in sets. Therefore, the current semantic web must be extended by the mathematical way of thinking in order to meet the needs of mathematicians. Semantic tools must support the work flows of mathematicians.