How hard is it to go back to English, from Lean? Just as hard as going from English to Lean?
If it is easier to convert backwards, maybe the AI can at least describe what the equations mean…