I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced

I'm not an expert but I'd say based on my experience with Lean so far, the answer is yes. eg. I have entered some proofs from the Lean guide and then replaced tactics with `apply?` which searches for tactics to meet the goal, and eg. reduced this example from the guide: theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := fun hpq : p ∧ q => have hp : p := And.left hpq have hq : q := And.right hpq show q ∧ p from And.intro hq hp To this: theorem and_commutative' (p q : Prop) : p ∧ q → q ∧ p := by exact fun a ↦ id (And.symm a) Presumably the same thing could be done for each part of a more complicated proof and could be done so at each step automatically.