In a recent interview, Terence Tao opined on this:

When you gave a talk about a different mathematical project, someone asked you if you wanted to formalize it, and you basically said that it takes too long.

I could formalize it, but it would take a month of my time. Right now I think we’re not yet at the point where we routinely formalize everything. You have to pick and choose. You only want to formalize things that actually do something for you, such as teach you to work in Lean, or if other people really care about whether this result is correct or not. But the technology is going to get better. So I think the smarter thing to do in many cases is just to wait until it’s easier. Instead of taking 10 times as long to formalize it, it takes two times as long as the conventional way.

I think he is trying to say that Lean proofs currently take 10 times as long as informal ones.