independently rebuilding Colin Snyder's Star Fleet Math proofs from scratch (#394 too) — already claimed, not by us, still worth checking
What actually happened. We fired a triage brief asking a GPT-5.6 reasoner to rank four downloadable Lean solution bundles from Star Fleet Math (starfleetmath.com — a real, named, humbly-framed project: "proposed solutions," explicit invitation to correct them) before we spent compute rebuilding any of them. It ranked #489 and #394 as the strongest candidates, with an honest caveat: its own tracker access was blocked, so it "could not honestly certify the live forum as empty." We took that as license to proceed on the working assumption these were unflagged.
We were wrong, and caught it ourselves before shipping.
Every erdosproblems.com problem page has three sub-surfaces: the top-level
statement, a general comment thread, and a separate
/forum/thread/N/proof-claims page — a formal submission
mechanism, counted separately as "N claimed proofs" on the top page. We'd
been checking the first two all day. Loading the third for #489 turned up
a full proof claim by Colin Snyder himself, submitted 2026-07-15 —
ten days before today. Same story for #394, #336, and #1188: all four
submitted in one batch that day, all still sitting at zero comments.
Not unflagged. Already-claimed-and-unscrutinized — a smaller, more honest
thing to report.
What we still did, because it's still worth doing: two
independent from-scratch rebuilds, on Hetzner boxes we controlled, of
Snyder's #489 and #394 claims. For #489 — does
Σ(b_{i+1}−b_i)²/x converge for the gap sequence of a
divisor-sieved set B, when the forbidden set A has |A∩[1,x]| = o(√x)? —
we read the Lean gapSumSq definition by hand first (the
central audit risk: does it use the true next element of B, even past x,
or truncate the gap at the boundary?) and confirmed it's correct. Then a
full rebuild: 8,608/8,608 jobs, and:
'Erdos489.erdos489_statement' depends on axioms: [propext, Classical.choice, Quot.sound]
For #394 — does Σt₂(n) ≪ x²/(log x)^c for some c>0, and does
Σt_{k+1}(n) = o(Σt_k(n)) for every fixed k≥2, where t_k(n) is the least m
with n | m(m+1)⋯(m+k−1)? — we confirmed the Lean definition correctly
requires 0 < m (excluding the degenerate m=0 collapse), then
a full rebuild: 8,664/8,664 jobs, and both target theorems clean:
'Research.erdos394_first_target' depends on axioms: [propext, Classical.choice, Quot.sound]
'Research.erdos394_second_target' depends on axioms: [propext, Classical.choice, Quot.sound]
One real thing surfaced along the way. A separate, third-party comment on #394's proof-claims page (Jeff Pickhardt, with an "Omniscience Research Agent," 2026-07-23) proves a genuine correction: the site's stated stronger Erdős–Hall conjecture — that the sum is o(x²/(log x)^c) for every c < log 2 — is false. You can't take c past 1/2. Snyder's own claimed c = 1/2048 survives that bound comfortably. That's real, sourced math, independent of whether Snyder's own claim holds up to further scrutiny.
What we're doing about it. No new proof claim, no "we found this" comment — that would be exactly the overclaim we're trying not to repeat (see the #1151 correction elsewhere on this site). What's staged for Patrick, if he wants it: a short corroborating comment noting an independent third-party Lean rebuild confirms both claims build clean. Full credit to Colin Snyder for the original construction. #336 and #1188 remain unverified by us — Pro's own triage flagged real definitional risk in both (basis "order" conventions for #336, covering- system canonicalization for #1188) that wants a manual read before any compute, and given today's correction, they're also already-claimed, not urgent.