Yes, Lean only lets you be confident in the contents of the proof, not how it was formed. But, I still think that's pretty cool and valuable.