Hacker News Reader

Comment by kurthr | Hacker News Reader

tl;dr Until someone can explain the proof in something under 100s of hours, it's not considered proven. It's not useful until someone uses IUT as a tool.

It reminds me of other fields of science (like genetics) where many people have made a similar "discovery", but one person finally discovers and reports the results so clearly (e.g. Gregor Mendel) that everyone recognizes them as the discoverer... even though others came before (e.g. Imre Festetics) with similar concepts.

View on HN

Mendel was a monk and high school teacher whose work (he spent a decade hybridizing pea plants in the monastery garden) was published in small regional sources and languished in obscurity for decades. Nobody at the time understood the importance of his work, and biologists continued under mistaken models of how inheritance worked. Decades later other botanists did similar experiments, and then stumbled over Mendel's papers, and credited him for first developing and experimentally validating the correct model. e.g. Correns http://www.esp.org/foundations/genetics/classical/holdings/c...

As far as I know Mendel's model was much simpler and more clearly defined than anything that came before.

Yes, exactly, he discovered it well enough that people who read his papers years later didn't need for it to be discovered again. I agree, those at the time of publishing didn't even consider it to be about inheritance, but those later did, because his careful work could be replicated... even though Imre Festetics coined the word genetic and did similar work on sheep in the same town many years before (he's mostly forgotten).

Could it be that someone, in some obscure regional mathematics journal already proved abc conjecture in 30 pages. No one took his work seriously enough, and his work would be discovered by accdent 100 years after publication?

I would sure be convinced by a Coq proof I couldn't understand. Professional mathematicians will face that kind of result eventually, if we keep progressing.

Counterexample: The Four Color Theorem (which states that any 2-dimensional map can be colored with four colors such that no two bordering countries have the same color). It is considered proven even though the proof involves a giant computer verification which certainly can't be explained in under 100s of hours.

I would expect one can reason about the program of the proof in less than 100 hours, which is essentially the proof.

> Counterexample: The Four Color Theorem (which states that any 2-dimensional map can be colored with four colors such that no two bordering countries have the same color). It is considered proven even though the proof involves a giant computer verification which certainly can't be explained in under 100s of hours.

There exists a proof of the Four Color Theorem by Georges Gonthier that has been verified in Coq:

> https://www.ams.org/notices/200811/tx081101382p.pdf

> http://www.cse.chalmers.se/edu/year/2015/course/DAT140/Gonth...

> https://mathoverflow.net/a/164949/12546

Reply on news.ycombinator.com