"Automated proof" means that the verification is automated. Actually automating the process of finding proofs is still mostly an open problem.

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.

No surprise there; it's why the software development industry is reluctant to adopt such techniques; nobody wants to write 5 times the amount of code, or take 5 times as long to get to the market.

> 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.

21 collaborators. Depending on how much time they each spent on it, he could have easily gone over budget.

Also, as it was all unknown stuff at the time, any estimation would have been made without prior experience.

How does that compare to the time it takes to write code vs test code? Maybe not quite that extreme, but test code is time consuming, and is essentially what theorem proving is.

How is test code related to theorem proving?