zlacker

>>nl+(OP)
This seems to be 2nd in row proof from the same author by using the AI models. First time it was the ChatGPT which wrote the formal Lean proof for Erdos Problem #340.

https://arxiv.org/html/2510.19804v1#Thmtheorem3

> In over a dozen papers, beginning in 1976 and spanning two decades, Paul Erdős repeatedly posed one of his “favourite” conjectures: every finite Sidon set can be extended to a finite perfect difference set. We establish that {1, 2, 4, 8, 13} is a counterexample to this conjecture.

>>menaer+Nb
that one was vibe-coded

Ai was given step-by-step already found proof, and asked "please rewrite in Lean"

---

here Ai did the proof itself