Hacker News Reader

Is it able to transpile to Coq/Lean/Agda/etc?

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

Reply on news.ycombinator.com