alt Hacker NewsSuch a result should be considered worthless: the proof is 10MB of Lean. (https://github.com/openai/PrimeGaps186).
I can't think of a single mathematical proof being anywhere close to ten million characters. For all you know, 90% of the proof could be useless, 8% would be writing out Shakespeare, and 1% abusing another bug in Lean. Humanity gets zero value from that, aside from "some bot seems to think it's 186". Unusable by anyone.
Replies
The human-written https://github.com/AxiomMath/PrimeGapsLib adds up to 4MB of Lean so it's that far off.
The proof of the classification of finite simple groups is bigger than that.
Yeah. Unless human can verify it, not sure if it is certain or useful.
Iirc some mainstream physycists never acknowledged quantum theory because they couldn’t accept that universe was that unintuitive and hard to understand.
Ditto ones that opposed Einstein’s general relativity.
You talk about modern math and worthlessness at the same time? That’s brave.
Terence Tao says something surprisingly similar in a recent talk (https://news.ycombinator.com/item?id=49056620 ) Not that the proof is worthless but that the value comes after it's revised into a cleanly understandable form and then canonicalized so that other mathematicians can use it.