Comment by heliumtera
11 hours ago
Isn't it bad faith to say no priors solutions was found when a solution published by erdos was ultimately found by the community in 10 minutes?
11 hours ago
Isn't it bad faith to say no priors solutions was found when a solution published by erdos was ultimately found by the community in 10 minutes?
Maybe, that's a decent point. I didn't realize it was that quick, I would have appreciated you mentioning that in your previous comment.
It does beg the question, if it was so easy to find the prior solution, why has no one posted it already on the erdos problems website?
That sounds like a great question. Why did no one bother to mention the problem was already proved and published by the author that proposed the statement 90 years ago?
Somehow an llm generated proof that consist of gigabytes upon gigabytes of unreadable mess is groundbreaking and pushes mathematics forward, a proof proposed by Erdos himself in 5 pages gets buried and lost to time.
Maybe one particular optics fuels the narrative that formal verified compute is the new moat and llms are amazing at that?
the proofs written by ChatGPT are necessarily reasoned about in plain language, and are a human-comprehensible length (that is what Tao did, since it hasn't been formalised in a proof-checking language); today, the many-gigabytes (or -terabytes) proofs (à la 4-colour theorem) are generally problems solved via SAT solvers that are required to prove nonexistence of smaller solutions by exhaustion.
and there is an ongoing literature review (which has been lucrative to both erdosproblems and the OEIS), and this one was relabelled upon the discovery of an earlier resolution