Comment by RossBencina

> Is there a way to read lean proofs noninteractively.

I'd like to see an answer to this question. I was looking into it the other day.

I found this: https://xenaproject.wordpress.com/2019/02/11/lean-in-latex/ Which gives a way to do the clicking-through outside the editor. And maybe gives some insight into how Lean people see things.