Writing mathematics in a formal language involves many tedious and difficult steps.

“So the point is, there's a, there are lots of, lots of steps when writing math in this formal language that become kind of tedious and difficult. One of Leo de Mora's ideas for Lean is it would have these little helper programs called tactics, which will automate some of those repeated steps, those kind of things, steps that happen regularly in proofs.”