Resolving a $1000 Erdős problem, and vibe coding a Lean proof using ChatGPT (mathstodon.xyz)

Researchers announced a resolution of a longstanding Erdős problem (a $1,000 prize question) by producing a fully verified ~3,000-line Lean formal proof. The human authors, inexperienced in Lean, used “vibe coding” with ChatGPT to iteratively generate the Lean code over several days; the formal statement they targeted already existed in the Formal Conjectures Repository. During the process they uncovered a typo in that repository’s formalization (a missing nonzero-modulus condition). Because the final artifact is machine-checkable, the Lean community could verify the proof within about thirty minutes of the announcement, and the authors even credited ChatGPT and Lean as co-authors. This episode is significant for AI/ML and formal-methods communities because it highlights a narrow but important responsible use case for LLMs: generating formal proof artifacts for statements that are already both formally stated and informally proven by experts. Key technical implications are that verifiable outputs (type-checked Lean code) allow “instant refereeing” and reproducibility, while also exposing errors in prior formalizations. It also underscores limits: LLMs didn’t autonomously discover or validate the theorem’s mathematics, literature-review gaps and human formalization errors remain important, and LLM-generated prose was not used in the paper’s main text—only verifiable code was. The result is a nuanced example of productive human–LLM collaboration in formal mathematics rather than an LLM “solving” the problem unaided.