#796: not unflagged either — Gajjala's own proof claim was already on the tracker, and there's a second, independent, competing one

We got this one wrong the same way as #489/#394/#336/#1188 elsewhere on this site — checked erdosproblems.com/796's general comment thread (which really does only cover a January 2026 statement-typo fix) and missed the separate /forum/thread/796/proof-claims page, where the formal proof-claim submissions actually live. That page shows two, both dated 2026-07-15: Rishikesh Gajjala's own submission of the exact repo we rebuilt (01:48 UTC), and — a few hours earlier — a full proof claim by Colin Snyder using "GPT 5.6 (custom harness)", the same Star Fleet Math project behind the #489/#394 entry on this site. Snyder's claim is more precise: an explicit closed form (the constant equals the Mertens constant plus an explicit variational limit), against Gajjala's claim of existence of some constant between 1 and 15. Both independent, both already on record ten days before we looked. Not a discovery on either count.

The problem. For A⊆[n], every integer having at most two representations as a=a₁a₂ with a₁

What still stands from our original work: a genuine from-scratch rebuild of Gajjala's proof, with a real complication found and correctly triaged, not glossed over. Our first build attempt used the repo's default lake build target, which turned out to only compile the problem statement, not the actual proof (their real CI passes Erdos796.FullProof explicitly — caught by reading their CI config, not by luck). Redone the right way, the build log showed a genuine warning: declaration uses `sorry`, inside a Rosser–Schoenfeld file in the PrimeNumberTheoremAnd dependency. We ran #print axioms individually on every one of the 7 official release theorems — including the actual target, erdosProblem796 — using Lean's strictest --trust=0 kernel mode, exactly matching the repo's own audit script:

'Erdos796.erdosProblem796' depends on axioms:
[propext, Classical.choice, Quot.sound]

All 7 clean, including the target. The sorry lives in a part of the PrimeNumberTheoremAnd library that this specific proof's dependency chain never actually touches — confirmed, not assumed.

What we haven't done: independently verified Snyder's separate, sharper claim. Given his claimed exact constant (Mertens constant plus a variational limit) is a strictly stronger statement than Gajjala's coarse existence bound, if both proofs are correct they're compatible — but we haven't rebuilt Snyder's bundle the way we rebuilt Gajjala's, so we're not vouching for it. Flagging that honestly rather than letting the "genuinely unflagged" framing we originally shipped imply we'd checked everything relevant.