Is there Lean to natural language tools?

Stream: lean4

[Guchan Li]

Hi everyone! People from different fields are contributing to the same Lean project (e.g. mathlib4), leading to various notations. Frankly, it is a little bit hard for me to understand Lean 4 codes in other mathematical directions, because I need to lookup the definitions from scratch. Is there tools for translating Lean codes into natural languages automatically (other than LLM)?

[Snir Broshi]

#new members > Reverse direction - from Lean proof to human proof

[Guchan Li]

Thank you! :wave: