I thought of this, but couldn't find a nice way to fit this into the syntax.

That is,

  Theorem: "some text"

is the same as

  Theorem:
  . "some text"

Thus it would be hard to distinguish a named theorem with one statement

  Theorem:
  . "some name"
  . "statement 1"

from an un-named statement with two statements:

  Theorem:
  . "statement1"
  . "statement2"

So for now I'm leaving the name in the metadata section, but I'm open to putting the title higher if I can come up with a nice way to do so.

I have read through this before, but thanks for sharing the link.

A Google Group has been created to discuss MathLingua and Mathematical Knowledge Management at https://groups.google.com/d/forum/mathlingua-discuss.

Everyone is welcome to join.

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.

If you prefer email, that’s cool too.

Sure, go ahead and set something up!

Cool. I've setup a Google Group at https://groups.google.com/d/forum/mathlingua-discuss.

Yes that would be nice. Thanks!

Awesome. I've setup a Google Group at https://groups.google.com/d/forum/mathlingua-discuss.

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 for the question. I have answered it in another question in the comments, and I'll update the docs to make the difference more clear.

It is already difficult to have a formalized math language with a level of formality that matches that found in papers.

The goal of MathLingua, at this time, is to match such a level of formality that is in math books and papers.

However, the syntax was designed to allow support for transpiling to a theorem proving language to be added at a later time. It is something, in the future, that I would like to do, if possible, but I don't have a time estimate if/when it will be available.

I recommend to check also Decucteam[1][2] projects, they also convert between different formats. Even as they focus on mathematical logic mostly, it still can be useful to check.

[1] http://deducteam.gforge.inria.fr

[2] https://github.com/Deducteam

Thanks! I wasn't sure how people would feel about the syntax, and I'm glad you like it.

Thanks for the support! Yes, that is one of the goals, to make it really easy to find what is known in mathematics and contribute to that knowledge base. I have https://mathlore.org which is a demonstration of how such as system could work.

Thanks for the links. I was not aware of Thomas Hale's research even though I searched extensively to try to find related work.

His descriptions of what he wants to attain align with what I would like, a formalized way to describe what is known in mathematics.

He also describes how this can be used for machine learning, and area that I am also pursuing, but my results are still in an exploratory state.

Either way, I am really glad others are looking into this area too. I think it is something that will be very beneficial to the math community.

This is an area of my interest too, esp. if one can find something that is actually useful for a practicing mathematician. I mentioned Hales' project but based on their github project progress (a postdoc of his did some exploratory work) they seemed to have hit some road blocks, which is an example of this problem being hard. I don't know what your background is. If you are interested in further discussion I would be happy to p.m. over email.

I have a PhD in mathematics, I am a software engineer working at Google, and have practical experience with programming language design and usage.

MathLingua is not a Google product and is not affiliated with Google in any way. Instead it is my own work I am exploring at the intersection of math, computer science, language design, and natural language processing.

It would be great to chat more over email. My email can be found on my github page https://github.com/DominicKramer. Let me know if you have problems getting it.

This also reminds me of mmt https://uniformal.github.io/ The primary developer of that recently gave a talk about it here https://vimeo.com/421123419