then
> plan to formalize his proof ... estimated it would take 20 years
so is it just me, or is the "work" of the normal proof only took 1/5th of the time it took for the automated/formalized proof?! that seems counter-productive imho...
Formal proof software will help you on small stuff, but you will still do most of the work, and you have to go much more in details, so it takes much more time.
It took 5 times to make it not a hunch but a real demonstration. If that's counterproductive or not remains as a something opinable.
> make it not a hunch
That's not what automation is doing; it doesn't turn conjectures into proofs. It finds mistakes in proofs; those proofs are not "hunches" but rigorous efforts.
Something which finds faults demonstrates is value mainly whenever it finds a fault. (Or at least that is a very easy perception to slide into.)
Note that we now actually know there is no more fault, because formalization is complete.
Also, as it was all unknown stuff at the time, any estimation would have been made without prior experience.