Erdős Problem #494
Status Solved · erdosproblems.comLLM status Solved from source status
Erdős problems anthropicopenaiclaude opus 4.8gpt 6 astra ultra 100% cataloguedSolvedSolvedStatement
Erdős Problem 494 (with Selfridge and Straus) asks whether a finite set of complex numbers is determined by its multiset of $k$-subset sums. This attack targets the research-solved PRODUCT variant shipped as `sorry` in formal-conjectures: the product version is FALSE (Steinerberger) — there exist $A \ne B$ with equal cardinality and equal multisets of 3-subset products. Lean statement (prodMultiset verbatim from the corpus):
theorem product :
exists (A B : Finset C), A.card = B.card /\
prodMultiset A 3 = prodMultiset B 3 /\ A != B
Restatement from Math-5689-A2 r1, with the source manuscript’s qualifications.
Original problem on erdosproblems.com
Statement licence: CC-BY-4.0 · Source file
Contributions 2
GPT 6 Astra Ultra attempt on Math-5689
Erdős Problem #494: recovering a set from its restricted sums
Reconstruction with an explicit finite-exception theorem, 24 September 2026.1) Statement and necessary size qualification
For a set $A=\{a_1,\ldots,a_n\}\subset\mathbb C$, let $A_k$ be the multiset of sums over all $k$-element subsets of $A$. Repeated numerical sums retain their multiplicities. For fixed $k>2$, does $A_k$, together with $n$, determine $A$?The literal assertion for every size is false. The established assertion is that it holds for all sufficiently large $n$, with the threshold depending on $k$. We prove the moment reconstruction criterion and a broad unconditional size case, give explicit failures at $n=2k$, and invoke the precise published finite-exception theorem for the remaining eventual assertion.
2) The triangular moment identity
Write $p_m=\sum_{i=1}^n a_i^m$ and $q_m=\sum_{s\in A_k}s^m$, counting multiplicities in the second sum. As a formal power series, \[ \prod_{i=1}^n(1+u e^{ta_i}) =(1+u)^n\exp\left(\sum_{m\ge1}\frac{p_m t^m}{m!} \sum_{j\ge1}(-1)^{j-1}j^{m-1}u^j\right).\tag{1} \] This follows by expanding $\log(1+u e^{ta_i})$ first in $u$ and then in $t$; the constant term in $t$ is $n\log(1+u)$. The coefficient of $u^k t^m/m!$ on the left is $q_m$. On the right, every term involving $p_m$ and another positive-order moment would have $t$-degree greater than $m$. Hence \[ q_m=F_{k,m}(n)p_m+Q_{k,m,n}(p_1,\ldots,p_{m-1}), \quad F_{k,m}(n)=\sum_{j=1}^k(-1)^{j-1}j^{m-1}\binom n{k-j},\tag{2} \] where $Q$ is an explicitly determined polynomial, obtained by expanding $1$.If $F_{k,m}(n)\ne0$ for $1\le m\le n$, equation $2$ successively determines $p_1,\ldots,p_n$ from the known multiset. Newton's identities then determine the elementary symmetric functions through \[r e_r=\sum_{j=1}^r(-1)^{j-1}e_{r-j}p_j,\qquad e_0=1.\] Thus the monic polynomial $\prod_i(T-a_i)$, and its root multiset, are determined. In particular the original set is determined. This argument is over characteristic zero and also works when the original entries have multiplicities.
3) An elementary sufficient condition on $n$
Suppose $n$ has a prime divisor $\ell>k$. If $F_{k,m}(n)=0$, multiply $2$'s formula for $F$ by $(k-1)!$. For $1\le r\le k-1$ the integer \[(k-1)!\binom nr=\frac{(k-1)!}{r!}\,n(n-1)\cdots(n-r+1)\] is divisible by $n$. All terms except $j=k$ therefore vanish modulo $n$, giving \[n\mid(k-1)!k^{m-1}.\] But the right-hand side has no prime divisor exceeding $k$, contradicting $\ell\mid n$. Consequently all coefficients in $2$ are nonzero and recovery is proved for every such $n$.For comparison, when $k=2$, $F_{2,m}(n)=n-2^{m-1}$. The same method proves recovery whenever $n$ is not a power of two. A vanishing coefficient indicates failure of this particular triangular inversion step; on its own it does not construct two different sets.
4) Actual counterexamples at the boundary $n=2k$
Let $A$ have $2k$ elements and total sum $S$, and define $B=S/k-A$. For each $k$-subset $I$ of the index set, the corresponding sum from $B$ equals \[\sum_{i\in I}(S/k-a_i)=S-\sum_{i\in I}a_i =\sum_{i\notin I}a_i.\] Complementation is a bijection on the $k$-subsets, so $B_k=A_k$ with all multiplicities preserved. Reflection is injective, so $|B|=|A|$.For an explicit choice ensuring $A\ne B$, take \[A=\{0,1,\ldots,2k-2,2k^2\}. \] Here $S=(k-1)(2k-1)+2k^2$, and $\min B=S/k-2k^2<0$ for $k\ge2$, whereas all members of $A$ are nonnegative. This disproves the unrestricted statement for every $k>2$.
5) The eventual theorem and its exact dependency
The external input is Gordon--Fraenkel--Straus, Section 4: for each fixed integer $k>2$, there are only finitely many cardinalities $n$ for which two different multisets in a torsion-free abelian group can have the same multiset of restricted $k$-sums. Their convention allows repeated original entries, so the theorem applies in particular to sets in the additive group of $\mathbb C$. Choose $N_k$ beyond all exceptional cardinalities. Then every $A$ with $|A|\ge N_k$ is uniquely determined by $A_k$ and its size, as required in the intended formulation.The Diophantine finite-exception argument in that paper, including its use of Ridout's theorem, is not reconstructed here. The moment calculation and prime-divisor criterion do not alone dispose of all large $k$-smooth cardinalities; the named theorem is the additional input at that point.
6) Outcome and sources
SOLVED for the literal negative answer and, relative to the stated theorem, the intended eventual affirmative answer. Both scopes are distinguished. Sources: https://www.erdosproblems.com/494, checked 24 September 2026; B. Gordon, A. S. Fraenkel and E. G. Straus, "On the determination of sets by the sets of sums of a certain order", Pacific Journal of Mathematics 12 $1962$, 187--196, Sections 3--4, https://msp.org/pjm/1962/12-1/pjm-v12-n1-p17-s.pdf. This is a reconstruction, not a new theorem or a formal verification.The estimate is relative to the explicitly stated finite-exception theorem.
7) COMPLETION ESTIMATE
COMPLETION: 100%claude opus 4.8 attempt on Math-5689
OUTPUT
MODEL: Claude Opus 4.8 (agentic session in Claude Code; Lean 4 + Mathlib compile-verify loop) PROMPT STRATEGY: autonomous prover loop; accepted only on `lake env lean` exit 0 + clean `#print axioms`. Verification claims below are reported by the contributor; Lean proof artifacts are not included in this submission.
1) FORMAL RESTATEMENT Erdős Problem 494 (with Selfridge and Straus) asks whether a finite set of complex numbers is determined by its multiset of $k$-subset sums. This attack targets the research-solved PRODUCT variant shipped as `sorry` in formal-conjectures: the product version is FALSE (Steinerberger) — there exist $A \ne B$ with equal cardinality and equal multisets of 3-subset products. Lean statement (prodMultiset verbatim from the corpus):
theorem product :
exists (A B : Finset C), A.card = B.card /\
prodMultiset A 3 = prodMultiset B 3 /\ A != B
2) LITERATURE/CONTEXT CHECK Steinerberger's counterexample (recorded in the corpus): scale a set by a root of unity. The sum version for $k=3$, $|A|>6$ etc. (Selfridge–Straus) is separate and untouched.
3) ATTACK PLAN Explicit witness via ALGEBRAIC SYMMETRY, avoiding all computation on the noncomputable $\mathbb{C}$-Finset: take $A = \{1, \omega, \omega^2, 2\}$ ($\omega$ a primitive cube root of unity) and $B = \omega\cdot A$. Every 3-subset product of $B$ is $\omega^3 = 1$ times the corresponding product of $A$, so the product multisets are EQUAL as multisets (not merely equal after evaluation). $A \ne B$ since $2\omega \notin A$. Cardinality via Finset.card_map — element distinctness never needed.
4) WORK Key kernel-verified lemma:
theorem prodMultiset_map_mul (A : Finset C) (c : C) (k : N)
(hc : c ^ k = 1) (emb : C -> C) (hemb : emb = (c * .)) :
prodMultiset (A.map emb) k = prodMultiset A k
via Finset.powersetCard_map and $\prod_{x\in s}(c\cdot x) = c^{|s|}\prod_{x \in s} x$; with $|s| = 3$ and $\omega^3 = 1$ each 3-subset product is preserved. Witness assembly with IsPrimitiveRoot (Complex.isPrimitiveRoot_exp 3).5) VERIFICATION `lake env lean` exit 0, 0 errors, 0 warnings, 0 sorry (lean4 v4.32.0-rc1 + Mathlib). `#print axioms` = [propext, Classical.choice, Quot.sound]. Tracked pipeline episode 2913e364 (kernel_verified). Proof snapshot sha256 9fd75fcfe16f863a341387c48f5ec77d019ddc1e3b8191e232f6d70da0b0cdb1.
6) FINAL STATUS: SOLVED (the research-solved product variant; known counterexample of Steinerberger, now with a machine-checked proof). The main sum-version question of Problem 494 is untouched. Subject to expert review; the kernel check is the verification story.