---

Claim. For all integers $2\le k<n$,

$$\left\lfloor\frac{n-2}{k-1}\right\rfloor(n-k+1)-1 \le g(k,n)\le \left(\left\lceil\frac{n-1}{k-1}\right\rceil-1\right)n-1,$$

and $g(k,n)$ is determined exactly when $k-1$ divides one of $n$, $n-1$ and $n-2$. For fixed $k$ both bounds are $(1+o(1))\,n^2/(k-1)$ as $n\to\infty$, so $g(k,n)\sim n^2/(k-1)$, which answers the question of Problem 433 affirmatively in the regime of fixed $k$; the same bounds give the asymptotic uniformly whenever $k=o(n)$. Erdős and Graham's formulation leaves the regime unstated, and the site's commentary reads it as fixed $k$ with $n\to\infty$, the reading this page settles. The result is J. Dixmier, Proof of a conjecture by Erdős and Graham concerning the problem of Frobenius, J. Number Theory 34 (1990), no. 2, 198--209; the page's date is the first day of the issue month, the only publication date recorded. The paper is not held by this corpus; the statement is taken from the site's commentary, from the site's thread and from the Lean development below. The site's commentary prints a floor in the upper bound; the thread post of 2026-02-24 reports that the site's commentary misprints the bound and that it should carry ceilings, and the Lean development proves the ceiling form, which is the form stated above. The earlier bounds $g(k,n)<2n^2/k$ and $g(k,n)\ge n^2/(k-1)-5n$ are Erdős and Graham's, on the corpus's card of their 1972 paper. The paper's Theorem 2, a lower bound on the number of representable integers in each interval $((j-1)n,jn]$, is the input of Kiss's solution of Problem 434, recorded on its page.

Acceptance. The paper is a refereed publication in the Journal of Number Theory, the refereed evidence. The site's curator, T. F. Bloom, labels the problem proved and credits Dixmier's paper with the proof; that documented acceptance is the reviewed evidence. The thread's remark of 2025-10-29 that the exact value is known only when $k-1$ divides $n$, $n-1$ or $n-2$ concerns the exact value, not the asymptotic question the problem asks.

Formalization. On 2026-02-24 the forum user JoshuaB reported a Lean formalization of Dixmier's Theorems 1 and 2 conditional on Kneser's addition theorem, made with the help of the AI systems Gemini 3.1 Pro, Gemini 3.0 Flash, Claude Sonnet 4.6, Project Numina and Aristotle; on 2026-05-29 the forum user JakeMallen reported that Claude Opus 4.8 had made the proof unconditional, in the repository Jayyhk/erdos-lean. Its file problems/433/Erdos433.lean (Lean 4.29.0; 6,650 lines at the pinned commit of 2026-08-27) vendors the Bakšys–Dillies proof of Kneser's theorem, proves theorem_1, the two-sided bounds above, and theorem_2, and derives erdos_433: for each $k\ge2$, $g(k,n)/(n^2/(k-1))\to1$. A closing comment records the axioms propext, Classical.choice and Quot.sound. The file's comments map its lemmas to Dixmier's, so it is a formalization of this paper's result and is recorded here rather than on its own page. The formal-conjectures statement erdos_433 (file added 2026-09-02), linked above as a record, states the asymptotic for every $k\ge2$, is tagged research solved, and names no formal proof. The Lean suffix of the site's label refers to this development. Nothing was built, replayed or audited here, so formalized is not listed.