One thing Lean inherits from mathematics is the use of opaque notation. It would be nice to inherit some readability from programming.

Paperproof is an effort in one direction (visualization of the logic tree)

https://paperproof.brick.do/lean-coq-isabel-and-their-proof-...