---

Claim. For every $k>2$ the multiset $A_k$ of the sums of $k$ distinct elements, together with $|A|$, does not determine sets of size $2k$: there are two distinct sets $A,B\subset\mathbb C$ with $|A|=|B|=2k$ and $A_k=B_k$. The Lean development Erdos494.lean in Boris Alexeev's repository of Lean proofs, added on 2026-08-16 and linked above at a pinned commit, proves this as its theorem card_eq_2k, stated as ∀ k > 2, ¬ Erdos494Unique k (2 * k) in the namespace of the formal-conjectures variants: it takes a set $A$ of size $2k$ with sum $0$ and its negative, whose $k$-fold sums agree because each $k$-sum of the negative is minus a $k$-sum of $A$, which is the complementary $k$-sum. The file's header calls it a formalization of a solution to Problem 494, names Basil Gordon, Aviezri S. Fraenkel and Ernst G. Straus as informal authors and the formal-conjectures authors as statement authors, and names the AI systems Codex and GPT-5.6 Sol as its formal authors. The repository's index Erdos494.md describes the file as "a formalized proof of Erdős Problem 494", and the header's list of URLs points to the formal-conjectures statement file whose variant it proves.

Why it is rejected. It answers the site's wording, not the corrected Statement. Its only theorem, card_eq_2k (with the alias card_eq_2k_counterexample), proves that uniqueness fails at $|A|=2k$ for every $k>2$, Tao's observation and Theorem 3 of Selfridge and Straus; the file's own section heading reads 'The literal problem has a negative answer'. Problem 494 judges its corrected Statement, which asks about all sufficiently large $|A|$ and excludes that size, so the theorem settles no instance of it. The file's header and the repository's index call it a formalization of a solution to Problem 494, which is why it holds a claim page rather than a mention.

Standing. Rejected. The file is third-party work that this corpus has not built or audited, so it gives a formalization link and no formalized evidence, and it does not prove the theorem of Gordon, Fraenkel and Straus that its header names, which is recorded on [[problems/additive_combinatorics/E0494/claims/1962_03_01_gordon_fraenkel_straus|their claim page]].

Depends on. No page of this wiki.