Lean2LaTeX

Stream: general

[Razz]

Hey everyone. Does anyone know of a non-AI way of mapping Lean code/logic to formal english mathematical statements? I found this Phrasebook by Tao but I'm unsure if something properly does this already. If not, I will have to build it.

[Markus Himmel]

This is sometimes called informalization. There is some work in this direction, see for example these slides.

[Lua Viana Reis]

for printing expressions, there is also https://github.com/kmill/LeanTeX