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.
