> 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...
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.
It looks counterproductive when it's not demonstrating informal work to be false.
> 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.)
And a fault was found! The original proof, as published, is incorrect. The error and the fix was published in "A revision of the proof of the Kepler conjecture" (2009). https://arxiv.org/abs/0902.0350
Note that we now actually know there is no more fault, because formalization is complete.
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.