---

Claim. For $r\ge2$ let $h(r)$ be the largest finite exact order of an asymptotic basis of order at most $r$. The development states that this maximum is attained for every $r$ and that

$$\lim_{r\to\infty}\frac{h(r)}{r^2}=\frac13,$$

which would answer Problem 336. The site's statement glosses a basis of order $r$ as one in which every large integer is a sum of at most $r$ elements, so its $h(r)$ ranges over bases of order at most $r$: this is the claimant's formulation, which the claimant identifies with the function $X(r)$ of Erdős and Graham studied by Grekos, Nash and Plagne. Plagne defines $X(h)$ as the largest exact order of $\mathcal A\setminus{a}$, over exact bases $\mathcal A$ of integers bounded below of order at most $h$ and elements $a$ whose removal leaves a basis. Adjoining $0$ gives $h(r)\le X(r)$; the reverse inequality is the claimant's argument. Erdős and Graham's own notation of 1980 restricts the maximum to bases of order exactly $r$ (their $g(r)$, with the order the least such $r$); for that function the claim gives only $\limsup g(r)/r^2\le1/3$, since $g(r)\le h(r)$. This page records the claimant's formulation. The claimant's bundle argues, in its statement audit, that the problem's "order $r$" means order at most $r$, and checks by padding representations with zero that its function equals $X(r)$; the argument is the claimant's. The author says periodic bases give the lower bound; that bound is prior art, as the site's remarks record: Grekos [Gr88] proved $\liminf h(r)/r^2\ge1/3$ and Nash [Na93] $\limsup h(r)/r^2\le1/2$, with Erdős and Graham [ErGr80b] before them bracketing the ratio between $1/4$ and $5/4$ and Plagne [Pl04] sharpening the lower-order terms. The new content is the matching upper bound. By the author's account the question is transferred to a finite cyclic group $G$; a search over dyadic scales locates one at which a certain set has doubling constant less than $9/4$, which places the extremal configuration in a lattice generated by two elements, and there an inequality $3\lvert G\rvert\le(H+2)^2$ between the group's size and the exact order $H$ is what produces $1/3$; the remaining cases are handled by classifying the three-element sets with exactly five distinct pairwise sums. The author writes that the route began from an argument they attribute to Lev (2020) and that formalizing it exposed two gaps in that printed proof: a count of differences that confuses ordered with unordered pairs, which the set $\{0,1,3\}\subset\mathbb{Z}/6\mathbb{Z}$ refutes, and an endpoint configuration $\{0,x,2x\}$ the proof omits; the author supplies new arguments for both.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

For $r\ge 2$ let $h(r)$ be the maximal finite exact order over all asymptotic bases of order at most $r$. We claim the limit exists and [\lim_r\frac{h(r)}{r^2}=\frac13.] Proved in Lean 4 / Mathlib; the final theorem gives both existence of each maximum and convergence. Standard axioms only, no sorry. Idea: periodic bases give the lower bound. For the uniform upper bound, the problem transfers to finite cyclic groups; a dyadic argument finds a scale with doubling below $9/4$, and the extremal case reduces to a two-generator lattice picture whose area inequality $3|G|\le(H+2)^2$ produces the constant $1/3$. The case analysis closes with a full classification of three-point sets with five double sums. Our route began from Lev's 2020 argument, but formalisation exposed two genuine gaps in the printed proof (an ordered/unordered difference count, contradicted by ${0,1,3}\subset\mathbb{Z}/6\mathbb{Z}$, and a missing endpoint case ${0,x,2x}$); both are repaired by new arguments. Notes: The value $1/3$ and the periodic lower construction are prior art; the contribution is the sharp uniform upper bound, the two repairs, and the machine-checked certificate including existence. Verify: run the included checker (SHA-256 manifest, 8,729 jobs, rejects sorry/admit/project axioms); final axiom print exactly [propext, Classical.choice, Quot.sound].

Standing. Claimed. The result was posted on 2026-07-15 as a solution page with a downloadable Lean 4 project (the preprint and formalization links; neither carries a commit pin) and entered the same day on the site's proof-claims thread (the discussion link), where it had no comments as of 2026-10-06; the site's label is OPEN (page last edited 2025-10-28), no named mathematician has examined the proof and there is no refereed publication. The author credits GPT 5.6, run in a custom harness, with the work. The final declaration is Erdos336.problem336 : HasProblem336Value (1/3 : ℝ), where HasProblem336Value c says that an extremal function exists and that $h(r)/r^2\to c$ for every extremal function; the project is built on Lean 4.31.0 and a pinned Mathlib revision, and the author's checker reports a manifest of 191 source files, 8,729 build jobs, no sorry or admit, and the axiom closure propext, Classical.choice, Quot.sound. Nothing was built or audited in this corpus: the definition IsExtremalFunction, and with it the formal reading of basis, order and exact order, has not been compared with the problem's wording, so no formalized evidence is listed and the problem's standing stays claimed.

Depends on. Nothing in this wiki.