---

Claim. Submitted to the proof-claim tab of Problem 796 on 2026-07-15 (01:50 UTC) by Colin Snyder as a full proof claim, declaring the use of GPT 5.6 in a custom harness. The claim answers the question yes: with $g_3(n)$ the largest size of $A\subseteq\{1,\ldots,n\}$ in which every $m$ has fewer than three representations $m=a_1a_2$ with $a_1<a_2$ in $A$, the normalized residual

$$\frac{g_3(n)-n\log\log n/\log n}{n/\log n}$$

converges; the summary writes its limit as the sum of the Mertens constant and the limit of an explicit variational sequence. The idea, in outline: primes and near-primes supply the main term; the second-order term trades smooth numbers kept below a threshold against the budget of multiplicative collisions; for the upper bound, two lemmas (one on the smooth remainder, one on an extracted tail) charge whatever an admissible set has beyond the main term to that budget, and for the lower bound a construction reaches the same variational quantity. The claim's own note says the formal statement was checked quantifier by quantifier against the site's text, with squares excluded by $a_1<a_2$. The write-up is the Star Fleet Math solution page linked above (the tab's proof link), which as of 2026-10-07 heads its report "accepted 2026-07-14", the basis for that link's date and the company's own acceptance, not a public posting date shown; it names no human author; it states the closed theorem Erdos796.erdos796_statement, the two gate lemmas and an axiom audit reporting propext, Classical.choice and Quot.sound; and it carries an unsigned referee section and a report of a re-verification on separate hardware, both the company's own and neither an outside review. Nothing on this page rests on the contents of the downloadable archive (the tab's formalization link).

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:

We claim the answer is yes: the constant $c$ exists, and equals the Mertens constant plus an explicit variational limit. Formally, with $g_3(n)$ the largest size of $A\subseteq{1,\dots,n}$ such that every $m$ has fewer than $3$ representations $m=a_1a_2$ with $a_1<a_2\in A$, the normalized residual [\frac{g_3(n)-n\log\log n/\log n}{n/\log n}] converges. Proved in Lean 4 / Mathlib (closed theorem Erdos796.erdos796_statement, hypothesis-free), standard axioms only, no sorry. Idea: the main term comes from taking primes and near-primes; the second-order term is a trade-off between smooth numbers kept below the threshold and the multiplication-collision budget. The upper bound is closed by two gates (a smooth-remainder gate and an extracted-tail gate) that convert every admissible set's excess into that budget; a matching construction attains the same variational value. Both meet at $c=M+\lim$ of the explicit variational sequence, where $M$ is the Mertens constant. Notes: The formal statement was pre-registered and audited quantifier-for-quantifier against the problem text ($a_1<a_2$, so $b=c$ squares are excluded, matching the site). The workspace contains incidental native_decide lemmas and the PrimeNumberTheoremAnd fork; the kernel axiom report ([propext, Classical.choice, Quot.sound], no sorryAx, no ofReduceBool) proves neither enters the final theorem's dependency cone, as documented in the bundle README. Verify: run check_answer/verify.sh (8,737 jobs), then "#print axioms Erdos796.erdos796_statement".

The formalization. The formal-conjectures file ErdosProblems/796.lean (at the commit the problem page pins) carries a formal_proof attribute naming Research/CanonicalTail.lean of an erdos-796 development in the repository williamjblair/lean-proofs at the commit linked above (committer date 2026-07-30), a re-hosted build of this development, and declares the problem research solved with the docstring that the rescaled error converges. The basis for the match: that repository's proofs.yaml at the same commit credits the proof to Colin Snyder of Star Fleet Math, names the file starfleet/erdos-796/Research/CanonicalTail.lean and the theorem Erdos796.erdos796_statement, and records that the PrimeNumberTheoremAnd project was substituted for the vendored copy omitted from the Star Fleet bundle; the formal-conjectures commit that added the attribute (7 August 2026) is titled as adding Star Fleet Math formal-proof links. So the development credits the claimant, and the link belongs on this page. At that commit, Research/Basic.lean defines the statement as ∃ c : ℝ, Filter.Tendsto normalizedError Filter.atTop (nhds c), and Research/CanonicalTail.lean proves erdos796_statement from two proved gate lemmas; Audit.lean prints the axioms of the final theorem. The 44 Lean files declare no axiom and contain no sorry; ten proofs in five modules use native_decide, which the claim text says do not enter the final theorem's dependency cone, a point unverified since this corpus has not built the development; the development imports Mathlib and an external Lean project on the prime number theorem. Nothing was built, kernel-checked or audited for statement fidelity in this corpus, so formalized is not evidence, and the collection's category is its maintainers' label, not an independent review of the whole statement.

Standing. Claimed. The site's label is OPEN (page last edited 16 January 2026, before the claim; proof-claim tab accessed 2026-10-06), while the formal-conjectures collection's category and attribute record this claim as a formal proof; the disagreement is recorded on the problem page. The claim carried no comments, and there is no curator comment, referee or named expert review. A second full claim of the same day, Gajjala's, also answers yes with the constant $1+M+\Gamma$; no comparison of the two constants is recorded. The problem's standing is claimed through these pending full claims.

Depends on. No page of this wiki.