math glossary

[holtzermann17]

@kohlhase @dginev: at the moment I see this issue as being at the intersection of PlanetMath, OMDoc, and NNexus.

• PlanetMath provides an initial corpus
• OMDoc provides a semantic representation language
• NNexus, using metadata from PlanetMath and other sites, begins to provide a light-weight "thesaurus" of mathematics terms
  • (... and @rspuzio, it also begins to provide a "cross-index" showing where the various terms are defined.)

Can we move from these ingredients towards a multilingual, semantic, computationally-interactive "mathematics glossary"? What else will we need?

I'm adding this to the "Future" milestone since we have our hands full stabilizing "normal" PlanetMath features. This is a fairly open-ended planning ticket.

• We might want to start by adding sTeX support to PlanetMath (sTeX integration in PlanetMath #358), although that itself is a complex agenda.
• We might also want to connect with with bibliography metadata (centralized bibliography #80), particularly if we think about things in the "cross-index" way

[rspuzio]

With respect to this and similar points like what we were
talking about with Florian a few weeks back, what I would
suggest is that sometime, perhaps during the summer
when we're not too busy and destracted, we could all
have a brainstorming session where we discuss our
ideas regarding artificial intelligence, linguistics, proof
checking, and the like and come up with some plans.

In the maenwhile, of course, this is as good a place as
any to make notes about or ideas; however, until we have
a chance to sit down together, discuss this, and get to
know each others' ideas, it's hard to see the big picture
behind all of this and figure out how to proceed.

[holtzermann17]

Maybe we can have the conversation with many of us in person at CICM 2013 (8-12 July, Bath, UK).

[rspuzio]

Maybe we can have the conversation with many
of us in person at CICM 2013 (8-12 July, Bath, UK).

I won't be able to be in England in July in person.
Is there be a way of including me remotely
since this is definitely a conversation I definitely
want to be a part of?

[holtzermann17]

Hopefully we can do something similar to what we did at the Columbia meetup
-- but this time, with you calling in remotely and Deyan there in person.