Does the formalization of major recent results in Lean imply in the future all math formalization will be automatic?

Math formalization has been hindered because it's so tedious. Will the future bring massive formalization because it can be automatic now?