Comment by heliumtera
10 hours ago
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