Comment by sanxiyn | Hacker News Reader

Comment by sanxiyn | Hacker News Reader

Parent Full thread

It is realistic in the sense that it has already been done! But it's still laborious in the extreme.

Kepler conjecture was stated in 1611 and had been unsolved since. Thomas Hales started a project to attack it in 1992. After six years of work, he announced the proof in 1998, in the form of 250 pages of argument and 3 gigabytes of computer calculation. He submitted it to Annals of Mathematics, one of the most prestigious math journal, for review. Reviewers and the author tried valiantly for five years, gave up, and published it in 2003 with a warning that while reviewers were 99% certain, it couldn't be completely reviewed.

Soon after getting this both rejection and acceptance, Thomas Hales announced the plan to formalize his proof to remove any uncertainty. It was enthusiastically received by automated theorem proving community. For a while Thomas Hales "shopped" for the prover tool to use and basically leaders of every significant provers tried to "sell" it to him. He decided on HOL Light, wrote the detailed plan for formalization, and estimated it would take 20 years. He actually carried out this plan, announced the completion in 2014, wrote the paper on formalization, and submitted the formalization paper, with 21 collaborators, in 2015. The formalization paper was published in 2017.

So there's that. The formal proof of Kepler conjecture is at the moment the most significant corpus of formalized mathematics in existence.

> After six years of work, he announced the proof in 1998

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

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?

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

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

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.

Reply on news.ycombinator.com