Pretty cool. Are you aware that there is a content markup part of MathML https://www.w3.org/TR/MathML3/chapter4.html ? There are other efforts geared towards math authoring as well if that is your focus,for example people have authored open textbooks using https://pretextbook.org .
Indeed. I decided not to use MathML for various reasons:
1. The syntax is horrible (for writing by hand).
2. I'm more interested in computation than presentation, so something closer to S-expressions along the lines of Mathematica feels more comfortable to me.
3. The progress so far on defining semantics for content MathML has failed to impress me.
Concretely, I think if you are trying to do semantic mathematics, you need an implementation of the semantics in software, not just a hand-written spec. Ideally this would be backed by a formal theorem proving system. So far I just do randomized testing using symbolic evaluation and interval arithmetic. See this writeup for more details: https://arxiv.org/abs/2003.06181
Your work looks really cool and your paper was a great read.
I too didn’t like the syntax of MathML, and I agree the semantics needs to be in the software.
For MathLingua I built a pattern matcher that is built in, but I haven’t tied MathLingua to a verifier.
I viewed these as separate things. This is because one can encode a statement but have a proof as a separate entity (which may be in a paper, digital, or verified form).
This allows one in mathlingua to express theorems and definitions from a book, for example, with references to the proofs in the book even though the results are not formally proven.
A layer on top of MathLingua would use MathLingua to formally verify statements. If this is needed, my plan is to leverage existing theorem provers for this.
Feel free to reach out by email if you want to chat more, or we can chat here. My email is on my github page https://github.com/DominicKramer.
Thanks! The symbolic computation aspect of your paper is very interesting. I would be very interested in checking out how conditional rewriting is achieved. Do you have more in depth writings on the theory and mechanics of your approach?
It looks like there is a lot of shared interest in this area.
fspeech, fdej, and others, what do you think of having a Google group, mailing list, or something similar to have a communication channel for anyone that wants to chat more?
If you are open to this (or have another suggestion) I’ll set one up and share the link here.