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

Also see: https://en.wikipedia.org/wiki/QED_manifesto

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