#796: the multiplicative-representation second-order term — genuinely unflagged, and a real sorry scare that resolved clean

This is the one that's actually unflagged — unlike three other candidates from the same scouting pass, where the authors had already posted in the thread. The visible comment history on erdosproblems.com/796 only covers a January 2026 correction to the problem statement itself (Quanyu Tang and Thomas Bloom fixing a typo'd exponent); no mention anywhere of Rishikesh Gajjala's construction. The tracker does show "2 claimed proofs" recorded — we don't know what those are or whether either is this one; the point is the public discussion doesn't reference it.

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

A real sorry, 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 — we caught this 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 did not wave this away. 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, by checking axioms on every individual theorem rather than trusting that the overall build succeeding meant anything.

Why this matters as a specimen, not just a result: "the build succeeded" and "the target theorem is sorry-free" are different claims, and only the second one is the real bar. A shallower check here would have either missed the sorry entirely (just trusting a green build) or over-reacted to it (assuming it contaminated the whole proof without checking). Both would have been wrong.