It's still a significant order of magnitude more time consuming to write a formal proof as you can't gloss over any details. Proof automation helps somewhat but

It's still a significant order of magnitude more time consuming to write a formal proof as you can't gloss over any details. Proof automation helps somewhat but the search space is so enormous it's not going to be feasible any time soon that you can avoid doing the difficult parts yourself. The formal proof for the Kepler conjecture involved around 15 people and was estimated to take around 20 years of work I think. If the summary for this proof is 300 pages, the formal proof would probably be 3K pages at least.