Another reason to formalize math is that formalized proofs become training material for automated mathematics.

Ultimately we want all of the math literature to become training material, but that would likely require automated techniques for converting it to formalized proofs. This would be a back-and-forth thing that would build on itself.