---

Claim. For integers $n\ge k\ge2$, the number of positive integers not representable as a sum of elements of $\{n-k+1,\ldots,n\}$ with repetition is the greatest such count over all $A\subseteq\{1,\ldots,n\}$ with $|A|=k$ and $\gcd(A)=1$: the theorem erdos_434 of the file problems/434/Erdos434.lean in the repository Jayyhk/erdos-lean (Lean 4.29.0; 6,353 lines at the pinned commit of 2026-08-27), which answers the question of Problem 434 affirmatively for $k\ge2$; for $k=1$ the gcd condition admits only $\{1\}$, as the formal-conjectures file notes. The forum user JoshuaB first posted the proof on 2026-02-24, produced by the AI system Aristotle from the formalization of Dixmier's Theorem 2 made for Problem 433; the posted file takes theorem_2 of that formalization as an axiom, and the post notes that the argument ultimately rests on Kneser's addition theorem, itself an axiom in that formalization at the time. The post says the system was not given Kiss's paper and that the argument differs from Kiss's: where Kiss computes the gaps of the candidate set and matches them against Dixmier's bound, the Lean proof shows that in every interval $((j-1)n,jn]$ the candidate set represents no more integers than any admissible set does (gaps_le_gaps_opt), and sums over intervals. On 2026-05-29 the forum user JakeMallen posted that Claude Opus 4.8 had made the proof unconditional, in the repository above, whose file vendors the Bakšys--Dillies proof of Kneser's theorem and proves Dixmier's theorem_2 inside; a closing comment records the axioms propext, Classical.choice and Quot.sound. The formal-conjectures statements erdos_434.parts.i and erdos_434.parts.ii state the same maximizer for $1\le n$ and $2\le k\le n$, are tagged research solved, and carry a formal_proof attribute pointing at the forum post of 2026-02-24.

Depends on. Dixmier's theorems: the development formalizes Dixmier's Theorem 2 and argues from it.

Standing. Claimed. Nothing was built, replayed or audited here: the fidelity of the Lean statement to the question was not independently reviewed by this project, the axiom comment was not reproduced, and no outside examination of the whole statement is published; the site marks forum comments as unverified. The Lean suffix of the site's label is not a documented independent review, so the page lists no formalized evidence. The problem's standing rests on the accepted page for Kiss's theorem, which this proof confirms by a different route.