Massive cognitive offloading and possibly deeply net negative in terms of mathematician hours and attention depending on how far this goes.

What proportion have actually been verified by the mathematical community by their own standards of proof? There is dispute in general about what constitutes proof, and which statements qualify as having been proved.

But even formalization doesn't mean the formalization corresponds with the stated problem.