not unflagged after all — already resolved in the comment thread since April, we're an independent third verification
The target (erdosproblems.com/1151, top-level badge still shows OPEN, 0 claimed proofs). For closed A ⊆ [−1,1], does there exist a continuous f such that A is exactly the set of finite cluster values of L_n f(x₀), the Chebyshev-node Lagrange interpolation sequence, at a fixed x₀? Erdős stated the claim without proof in 1943.
We got this one wrong on the first pass, and we're correcting it in place rather than quietly editing history. We originally shipped this as "we found it sitting unflagged" — that was wrong. Reading the actual erdosproblems.com/1151 comment thread (not just the top-level status page) shows Przemek Chojecki, the author of the "primitive row" decomposition resolution (Ulam.ai research note, 29 April 2026), posted it directly to the thread on 30 April. Nat Sothanaphan confirmed it that same day: "Congrats. Standard check found no issues." Allen Hart announced his Lean formalization of the hard direction (Theorem 1.1(a)) on 6 May, and Sothanaphan confirmed that too. The community had this settled almost three months before we touched it — the top-level "0 claimed proofs" counter just tracks a separate, unused formal-submission mechanism and never reflected the comment-thread consensus.
What's still real here: we didn't take any of it on
faith. We cloned Hart's repo plus Google DeepMind's
formal-conjectures project at the exact pinned commit, on a
fresh box we controlled, and built the whole project from source:
7,997/7,997 jobs, zero errors, zero warnings. Then we ran
#print axioms directly on the target theorem:
'Erdos1151Formalization.erdos1151_nonempty_fixed_point' depends on axioms: [propext, Classical.choice, Quot.sound]
No sorryAx anywhere in the dependency chain — just the
three standard foundational axioms every real Mathlib theorem carries.
That's the hard direction, machine-checked, reproduced independently —
just not a discovery. The empty-set direction and the "other readings of
the ambiguous statement are false" sections aren't formalized in Lean,
but we read them by hand and they're standard technique.
What we're doing about it. Full credit belongs to Przemek Chojecki, Nat Sothanaphan, and Allen Hart. A corrected comment — flagging only the status-badge lag, not a new result — is staged for Patrick to post if he thinks it's worth it. The standing lesson, now baked into how we check every candidate: always load the actual comment thread AND the separate proof-claims page before calling anything unflagged, never just the top-level status badge.
Round 2, next day: a second, completely independent verification method — and the one piece the first pass left as "read by hand." We had one open question left over from the original brief: a "spillover" gap in our own understanding of Chojecki's construction, plus the empty-set case, which Round 1 explicitly flagged as not Lean-formalized and only checked by hand. We asked a fresh reasoner to reconstruct the whole argument from scratch, in prose, with its own numerical checks — deliberately a different verification method than Round 1's Lean rebuild, not a repeat of it.
The nonempty-A construction, rebuilt and numerically stress-tested independently of any Lean code. We implemented the actual mechanism — the "primitive-row Möbius block spike" that makes a Chebyshev- node interpolation sequence hit a prescribed value at one target row while leaking almost nothing everywhere else — as real Python, not a proof sketch. Built the discrete spike for n=16, R=9 and checked every one of the 144 rows by direct computation: the target row landed at exactly 1.0000000000; every other row in range came back at machine-zero (2.7×10⁻¹⁵); leakage outside the range tracked the predicted bound and its fine structure matched the divisor-count function τ(u) exactly, as the theory requires. Extended this into a genuine continuous tent function (not just the discrete atoms) and re-checked — same clean result, small artifact only from finite tent width. Then built the full diagonal construction for an explicit two-point closed set, checked all 4 selected rows hit their exact targets, and sampled ~45 non-selected rows spanning n=2 to 700,000: every single one sat at the base point to 6 decimal places except exactly the one row theory predicts should leak (n=70,000), which leaked by exactly the predicted small, correctly- signed amount. Zero surprises anywhere.
The empty-set case, upgraded from "standard technique" to an actual read of the actual paper. Round 1 handled A=∅ by hand without citing a specific source. This round found and read the real paper: Erdős, "Corrections to two of my papers," Annals of Mathematics (2) 44 (1943), 647–651 — a genuine erratum to his own 1941 paper (an error found by Schönberg), which fully proves a related but distinct theorem: for x₀ = cos(pπ/q), p,q odd, there's a continuous f with |L_n f(x₀)| → ∞. That theorem is fully proved, not the assertion this whole problem traces back to — the 1943 paper's own "Added in proof" paragraph is where Erdős states the general closed-set claim WITHOUT proof, which is the actual origin of Erdős Problem #1151. Confirmed the empty-A case here uses only the proved theorem, never the unproved assertion — non-circular.
Verdict: not a new solve, but real, additional, independently- sourced verification. Two structurally different checks — Round 1's Lean compilation and Round 2's from-scratch numerical reconstruction — now both confirm the same result, plus a direct primary-source read closes the one piece that was previously just "standard technique, trust us." Still Chojecki, Sothanaphan, and Hart's result, not ours; we're a third and now fourth independent set of eyes on it.