---

Claim. Submitted to the proof-claim tab of Problem 796 on 2026-07-15 (04:48 UTC) by Rishikesh Gajjala as a full proof claim, declaring the use of GPT 5.6 Sol. The claim answers the question yes: there is a constant $c$, between $1$ and $15$, with

$$g_3(n)=\frac{n\log\log n}{\log n}+(c+o(1))\frac{n}{\log n},$$

and the repository's README states it as $c=1+M+\Gamma$, with $M$ the Meissel–Mertens constant and $\Gamma$ a variational constant defined by what the README calls the compatible-cofactor problem, together with the bounds $4/15\le\Gamma<13$ and $M<933/1000$. The summary describes the method as Erdős's of 1964 carried one order further: Erdős's counting settled the leading term, and the claim refines the bookkeeping through an optimization over families of cofactors, starting from the construction in Tang's 2026 note, which the problem page records. The manuscript is the PDF linked above; its proof is unverified.

Submission note. Posted to erdosproblems.com as a proof claim by Rishikesh Gajjala (account rishikeshgajjala) on 15 July 2026, giving "GPT 5.6 Sol" as the AI used:

There exists a constant c lying between 1 and 15 for which the problem statement is true. The proof uses the similar techniques as Erdős (1964). His bookkeeping only had enough resolution to handle the leading term, this proof goes a level deeper to handle this introducing the cofactor-family optimization. The starting point of the result is the Note by Tang (2026).

The formalization. In the repository rishigajjala/erdos-796-lean at the commit of 15 July 2026 linked above, Erdos796/Statement.lean encodes the problem as ∃ c : ℝ, HasSecondOrderConstant c, the convergence of ((g3 n : ℝ) - leadingTerm n) / secondOrderScale n to c; AUDIT.md records the author's release audit of seven theorems, #print axioms reporting propext, Classical.choice and Quot.sound, a build with --trust=0, the rejection of sorry, custom axioms and native_decide, and a dependency on 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.

Standing. Claimed. The site's label is OPEN (page last edited 16 January 2026, before the claim; proof-claim tab accessed 2026-10-06); the claim has no comments, and there is no curator comment, referee, named expert review or formalization audit. A second full claim of the same day, Snyder's, also answers yes with a constant written as the Mertens constant plus a variational limit; 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.