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.
