[CatsAreCool]

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.