Theorem providers should be treated as interactive. I don't know how Lean works but I know how Isabelle works. Reading Isabelle proofs in plain text (e.g. in the seL4 verification repository on GitHub) is completely useless. However, when you open one in Isabelle's IDE, you can click on any point in the proof and show the internal state of the verifier - what the current statement being proved is, so you can see how the last tactic modified it. You can also search for names of theorems and axioms by matching templates (e.g. "?a*(?b+?c)=?d" will match the law of distributivity and maybe some other stuff)