Mathematics Interchange Format

While typing up an interminable LaTeX formula, I started to muse on the idea of a universal mathematics interchange format. As we use computers more and more, we’ll have to slop formulas from one program to another, say from LaTeX to Maxima, or the distant future from LaTeX to our friendly neighborhood proof checker. It would be nice if there were some sort of standard format to represent formulas. For many purposes, LaTeX is that format, but LaTeX doesn’t preserve the semantic content of its formulas. For example, in the formula \int e^x dx, there is nothing that associates \int with dx.

MathML is probably closer, but I’m imagining something with a type system built on top of it. Sometimes when you write x y, you mean a polynomial in x and y, but sometimes you mean that x and y are elements of a nonabelian group multiplied together. An ideal interchange format should preserve that kind of semantic information, and in theory should allow you to check that your formulas are well-formed. It’s not that format would understand noncommutativity — that is the domain of computer algebra systems and theorem provers — but that the format would have a declaration that there is a type GroupElement, and that two group elements are multiplied using group multiplication. A more ambitious proposal would allow you to say that G has type Group, and that x and y have type GroupElement(G), while the group multiplication is a binary operation that preserves the property of being GroupElement(G). The free computer algebra system Axiom has a type system like this.