Comment by HappMacDonald

The real benefit is certainty.

If somebody makes a proposition and nobody is able to properly vet it, or if you just get a bunch of white heads to nod sagely and endorse it, very little prevents there existing a flaw that invalidates the whole thing which might go unnoticed for decades and ruin anything anyone tries to build atop of the result.

It's the same as security hardening in code, or checking for med interactions at the pharmacists. Or checking to make sure that the absolutely correct pill is being dispensed and not mixed up "Buttle/Tuttle" style with some other similar looking pill.

Formal rigor paved all the way from the proposition to the axioms is not 100%, nothing is 100%. But formal rigor paved over that entire distance redistributes all potential for error to the proof chain itself which is now far easier for a non-AI computer to verify, and to the strength of the axioms themselves which have had more scrutiny paid to them than any other statements in the history of mathematics.

Another important point is that you do not have to go all the way back to the axioms if someone else has already formally proved other complex statements you can rely upon instead, then you only have to pave the length of your driveway to the nearest communal road.