Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof
Boris Alexeev, Dustin G. Mixon
AI use, as the source states it
“With a healthy skepticism of this apparent oversight, and out of an abundance of caution, we used ChatGPT to vibe code a Lean proof of both Hall's and our counterexamples.”
Model: ChatGPT, as stated
Named here, or see a mistake? Write to privacy@papex.org.