---

Claim. Let $n=p_1^{k_1}\cdots p_t^{k_t}$ with $t\ge2$ distinct primes $p_i$ and exponents $k_i\ge1$. The largest integer not of the form $\sum_{1\le i<n}c_i\binom ni$ with integers $c_i\ge0$ is

$$\sum_{i=1}^{t}\sum_{j=1}^{k_i}(p_i-1)\binom{n}{p_i^{\,j}}-n,$$

the Frobenius number of the numerical semigroup generated by the binomial coefficients $\binom n1,\ldots,\binom n{n-1}$. This is Theorem 0.1(1)(b) of W. Hwang and K. Song, The Frobenius problem for numerical semigroups generated by binomial coefficients, arXiv:2412.17882, in the labels of v2 (2025-07-17) and v3 (2025-10-03). The first posting, v1 of 2024-12-23, titled The Frobenius problem for Binomial Coefficients, states the formula as Corollary 3.4, whose display omits the inner sum over $j$ that its Corollary 3.3, the Apéry set, carries. Part (1)(a) gives the Apéry set of the semigroup with respect to $n$, from which the Frobenius number follows; part (2) treats prime powers $n=p^m$, where the coefficients have common divisor $p$ and the paper computes the Frobenius number of the semigroup they generate after division by $p$. Since the integers that are not prime powers are exactly those with $t\ge2$, part (1)(b) answers the question of Problem 435, as Remark 0.2 of v3 states; v3's acknowledgment says the authors learned of the problem after the paper was written. No journal publication is recorded on the arXiv listing. The theorem and remark have been checked (the paper's library card); the proof of part (1) (Lemma 2.2, Theorem 3.2 and Corollary 3.3 of v2 and v3) was not checked.

The formula was found independently in the site's thread: on 2025-09-29 the forum user MichaelPeake conjectured it, on 2025-09-30 Stijn Cambie (the forum user StijnC) posted proofs that every larger integer is representable and that the formula's value is not, and later on 2025-09-30 a post identified this paper. The site's commentary credits that independent derivation. The posts are forum comments, not a dated manuscript, so they have no claim page of their own and are recorded here; the OEIS entry A389479 lists the sequence of values.

Acceptance. The site's curator, T. F. Bloom, labels the problem proved and credits this paper with the first proof; that documented acceptance is the reviewed evidence. The paper is a preprint, so refereed is not listed.

Formalization. On 2026-02-04 Boris Alexeev posted in the site's thread that Cambie's forum proof had been formalized by the AI system Aristotle. The file src/v4.29.1/ErdosProblems/Erdos435.lean of Alexeev's repository plby/lean-proofs (Lean and Mathlib v4.29.1; 2,393 lines at the pinned commit of 2026-06-30) declares itself a formalization of a solution of Problem 435, naming Hwang, Song, Peake and Cambie as informal authors and Aristotle and Alexeev as formal authors; its theorem erdos_435 states, for $n\ne0$ not a prime power, that the value above is the greatest integer outside the set of nonnegative combinations, and a closing comment records the axioms propext, Classical.choice and Quot.sound. The formal-conjectures statement erdos_435 (file added 2026-08-03,) is tagged research solved and carries a formal_proof link to this pinned file; the Lean suffix of the site's label refers to it. Nothing was built, replayed or audited here, so formalized is not listed.