Erdős #671 — Lagrange interpolation despite blown-up Lebesgue function

Statement

Given $a_i^n\in[-1,1]$ for all $1\leq i\leq n<\infty$, define $p_i^n$ as the unique polynomial of degree $n-1$ with $p_i^n(a_i^n)=1$ and $p_i^n(a_{i'}^n)=0$ for $i'\neq i$ ($1\le i'\le n$). Define $\mathcal L^n f(x)=\sum_{1\le i\le n} f(a_i^n)p_i^n(x)$, the degree-$(n-1)$ Lagrange interpolant of $f$ at the nodes $a_1^n,\dots,a_n^n$.

Part 1. Is there a sequence of node-arrays $a_i^n$ such that for every continuous $f:[-1,1]\to\mathbb R$ there exists some $x\in[-1,1]$ where $$\limsup_{n\to\infty}\sum_{1\le i\le n}|p_i^n(x)|=\infty \quad\text{and yet}\quad \mathcal L^n f(x)\to f(x)?$$

Part 2 (stronger). Is there such a sequence such that $\limsup_{n\to\infty}\sum_{1\le i\le n}|p_i^n(x)|=\infty$ for every $x\in[-1,1]$, and yet for every continuous $f$ there exists some $x$ with $\mathcal L^n f(x)\to f(x)$?

(erdosproblems.com/671, statement verified verbatim against the live page.) The quantity $\lambda^n(x)=\sum_i|p_i^n(x)|$ is the Lebesgue function of the array at stage $n$; its blow-up ($\limsup=\infty$) at a point $x$ is, by the uniform-boundedness principle, exactly the condition under which "most" (a comeager set of) continuous $f$ fail to converge at $x$ — the problem asks whether a specific $f$ can nonetheless dodge this failure everywhere it matters.

Facts

- Prize \$250; status OPEN on erdosproblems.com as of 2026-07-02, explicitly flagged "cannot be resolved with a finite computation" (site-owner belief; disclaimer notes the site may be unaware of resolving literature). - Falsifiable: no — this is an existence-of-an-infinite-sequence statement, not decidable by any finite computation; only a proof (or disproof) settles it. - Origin: Erdős, "Some of my favourite problems which recently have been solved" [Er82e, 1982]; Erdős, "Some unsolved problems" [Er97f, 1997]; also in the "Some of Paul's favorite problems" booklet [Va99, item 2.40] for the 1999 Budapest Erdős conference. - Tag on site: analysis. Official formalised-statement flag on erdosproblems.com is "No" (not present in google-deepmind/formal-conjectures) — the Lean artifact discussed below is an unofficial, forum-posted one, not merged into that repo. - Claimed candidate full solution (unverified). github.com/teorth/erdosproblems wiki "AI contributions to Erdős problems" (snapshot dated 30 Jun 2026) lists: [671] | Codex, GPT-5.5 Pro | 22 Jun, 2026 | ⚪ Candidate full solution (Lean), where the page's own legend defines ⚪ = Unverified (as opposed to 🟢 = Full resolution, 🟡 = Partial, 🔴 = Incorrect). This is corroborated by a forum comment on erdosproblems.com/671 (comment #7142, user "Leeham", undated but visibly the newest of 5 comments as of this check): "GPT Pro resolves both questions in the affirmative," linking an Overleaf writeup and "the Lean formalisation by Codex." - I decoded the Lean artifact myself (the live.lean-lang.org share-link fragment is lz-string-compressed base64, not readable via plain page fetch — I extracted and ran the exact decompression algorithm from the site's own bundled JS). The recovered 2829-line Mathlib file: - Contains theorem erdos_671 : ∃ X : ∀ n : ℕ, Row (n+1), (∀ n, (nodeSet (X n)).card = n+1) ∧ (∀ x A N, ∃ n ≥ N, A ≤ lebesgue (X n) x) ∧ ∀ f : C(Interval,ℝ), ∃ x, Tendsto (fun n ↦ interpolant (X n) f x) atTop (𝓝 (f x)) ∧ ∀ A N, ∃ n ≥ N, A ≤ lebesgue (X n) x — this is *exactly* the stronger Part 2 statement (Lebesgue function cofinally unbounded at every $x$, yet every continuous $f$ has *some* $x$ of convergence), which trivially implies Part 1. - Contains zero occurrences of the string sorry (checked directly on the decoded source). - The file's own docstring describes the construction technique (see Literature state / Attack surface below) and cites [erdosproblems.com/671] as its stated target, and references a companion file E671.tex (presumably the Overleaf writeup, whose rendered LaTeX I could not extract — Overleaf's read-only share view is client-rendered and not retrievable via plain HTTP). - Caveat, stated plainly: I did not compile this file (no Mathlib toolchain available in this session), so I cannot personally confirm it type-checks with no hidden sorrys introduced via macros/tactics that might elide errors, nor did I see a #print axioms output. The absence of literal sorry text and the exact-match type signature are strong but not conclusive evidence; treat as claimed, plausible, formally-typed, not independently verified by us or (per the AI-contributions wiki's own ⚪ marker) by the site maintainers either. - Related problems (Lagrange-interpolation/Lebesgue-constant cluster on erdosproblems.com, found via the analysis tag full-text scan): erdos/1129 (PROVED), erdos/1130 (PROVED), erdos/1151 (OPEN), erdos/1152 (OPEN), erdos/1153 (PROVED, 2026).

Literature state

No classical (pre-2026) literature resolving #671 was found. The problem sits in the classical theory of Lebesgue constants for Lagrange interpolation (Faber [Fa14] 1914, Bernstein [Be31] 1931, Erdős [Er61c] 1961: $\max_x\lambda^n(x) > (2/\pi-o(1))\log n$, tight via Chebyshev nodes) — that theory bounds the *global maximum* of the Lebesgue function from below, but #671 is a different, subtler pointwise/functional question about whether individual continuous functions can still converge at points where the Lebesgue function is locally unbounded. I found no paper that states or solves exactly this pointwise-exception question prior to 2026.

2026 development, unverified. As detailed in Facts, the erdosproblems.com forum (comment #7142, ~late June 2026, tied to the "22 Jun 2026" date on the AI-contributions wiki) records a claim that GPT-5.5 Pro / Codex produced a full affirmative answer to *both* parts, with a from-scratch explicit construction, and a Lean/Mathlib formalisation (theorem erdos_671, no sorry found by me). The construction (read from the Lean docstring, which I recovered by decoding the share-link): a triangular node array is built in countably many finite *stages* $k$. At stage $k$ a Level k is a finite family of pairwise-disjoint closed sub-intervals ("cells") inside a fixed "protected zone" $(-3/4,-1/4)$; shrinkLevel shrinks each cell so all "filler" node-rows stay Lebesgue-stable ($\lambda\le 2$) on it; then, per child cell, a "collision-pair" row is engineered (Collision.Data / pairRow) whose Lebesgue function is forced to exceed $k+1$ exactly at the child's centre while every other pair-row stays stable there; an "exterior" row (Exterior.closePairNode) separately forces $\lambda\ge k+1$ off all the cells; nextLevel shrinks once more so the exterior row is stable on the surviving cells. arrayRow n selects, for each $n$, whichever of filler/pair/exterior row has that many nodes; cofinal unboundedness of $\lambda$ *everywhere* is array_lebesgue_unbounded. For a fixed target $f$, a pigeonhole argument (exists_pair_abs_sub_le) picks, at each stage, whichever of the two colliding "close sample" nodes $f$ is closer to, producing a nested sequence of shrinking cells with a unique common point selectedPoint f, at which the interpolants are shown to converge to $f$ (arrayRow_converges_at_selectedPoint) via a polynomial-approximation + bounded-Lebesgue-function argument on the *stable* rows sandwiching the "bad" ones.

This is exactly the flavor of "adversarial per-point construction escaping a Banach–Steinhaus obstruction non-uniformly" that the two-part phrasing of Erdős's question invites, and the claim, if correct, resolves #671 completely in the affirmative (both parts). However: erdosproblems.com itself still lists the problem as OPEN, its own "problem status" widget shows "comment activity that has not yet been incorporated into the remarks" (i.e. an editor has not vetted/merged this claim into the page), and the github.com/teorth/erdosproblems AI-contributions tracker explicitly marks it ⚪ unverified, not 🟢 full resolution — the same tracker shows plenty of ⚪ entries elsewhere that were later downgraded to 🔴 "Incorrect" on other problems (e.g. #233, #358, #616, #647), so ⚪ should be read as "serious claim pending scrutiny," not "confirmed." Honest bottom line: partially-resolved in the sense that a specific, formally-typed, sorry-free-as-written candidate proof exists and is publicly checkable by anyone with Lean/Mathlib (paste the fragment at live.lean-lang.org), but it has not cleared independent verification by the site maintainers, by us, or (as far as I found) by any third party, as of 2026-07-02.

Adjacent, *already fully resolved* literature in the same cluster (useful technique donors, see Related): - erdos/1129 / erdos/1130: the node-choice minimizing/maximizing the global Lebesgue-constant functional is characterized by an *equioscillation* condition, proved by Kilgore–Cheney [KiCh76]/Kilgore [Ki77] (existence) and de Boor–Pinkus [dBPi78] (the max-min version) — classical variational/equioscillation technique, not obviously transferable (it optimizes a global functional, #671 needs a pointwise adversarial escape). - erdos/1153: Erdős–Turán's [ErTu61] question on whether $\max_{x\in[a,b]}\lambda^n(x)\ge(2/\pi-o(1))\log n$ for *any* fixed sub-interval $[a,b]$ was resolved in 2026 by Terence Tao, "Local Bernstein theory, and lower bounds for Lebesgue constants" (arXiv:2603.21453; erdosproblems.com/bibs/Ta26b), via a *local* Bernstein-type theory (localized exponential-type bounds via Nevanlinna's two-constants theorem + residue/logarithmic-potential estimates), extending Erdős's own global bound [Er61c] and Erdős–Szabados's [ErSz78] weaker local bound. This is the technically closest fully human-verified, published 2026 result on Lebesgue-function lower bounds, and its "local" machinery is a plausible independent-verification or alternative-construction toolkit for #671's blow-up requirement.

Attack surface

- Mode: literature-resolution / verification, not fresh derivation. The hard mathematical content already exists as a specific, checkable candidate; the highest-value action is *independently verifying (or refuting) the existing Lean proof*, not re-deriving from scratch. - Concrete first experiment: (1) fetch https://www.overleaf.com/read/gqmfrhsprtqm#59ac11 in an actual browser (or via Overleaf's API with a session) to recover the full LaTeX writeup text (I could not do this over plain HTTP — it is client-rendered); (2) paste the decoded Lean source (recoverable exactly as I did: percent-decode the #codez= URL fragment, then lz-string.decompressFromBase64) into a real Lean 4 + Mathlib toolchain (or live.lean-lang.org directly in a browser) and run #print axioms erdos_671 to confirm no sorry/Classical.choice-laundered gaps and that it elaborates against a genuine, unmodified Mathlib; (3) spot-check the informal construction against the formal statement's type (∀ x A N, ∃ n ≥ N, A ≤ lebesgue (X n) x for the everywhere-unbounded clause, and the Tendsto ... atTop (𝓝 (f x)) clause for convergence) to make sure the *formalized statement itself* matches Erdős's actual question (a documented failure mode elsewhere on the AI-contributions wiki is a technically-valid Lean proof of a subtly mis-stated theorem). - Oracle: mechanical and strong — Lean's type-checker either accepts erdos_671 against an honest transcription of the problem or it doesn't; the main residual risk is *statement-fidelity* (does the Lean Row/lebesgue/interpolant machinery actually encode Erdős's $p_i^n$/$\mathcal L^n f$/$\limsup$ correctly?), which requires a careful human (or LLM-assisted) read-through of the ~50 preliminary definitions before the main theorem, not just trusting the docstring. - Feasibility: high for us specifically — this is not "solve a famous hard open problem," it is "audit an already-produced, publicly-available, sorry-free-as-written Lean file and a linked LaTeX writeup, and either (a) confirm it compiles and faithfully formalizes the statement, in which case #671 is resolved and we could be first to report that clearly / contribute the missing rigorous verification, or (b) find the gap." This is squarely a literature-resolution/verification task, well within reach, and higher-value than most "genuinely open, unattempted" problems on the site precisely because someone else already did the hard derivation work.

Related

- erdos/1129 — same Lagrange-interpolation/Lebesgue-function setting; PROVED (Kilgore–Cheney/Kilgore, equioscillation characterization of the minimal global Lebesgue constant); technique (global equioscillation optimization) is a different flavor from #671's pointwise adversarial construction but shares all the base machinery ($\ell_k$, $\lambda$). - erdos/1130 — the max–min companion to 1129; PROVED (de Boor–Pinkus, same equioscillation characterization). - erdos/1151 — OPEN; asks (for Chebyshev nodes specifically) whether every closed $A\subseteq[-1,1]$ arises as the limit-point set of $\mathcal L^n f(x)$ for some continuous $f$ — a close cousin of #671's "engineer specific pointwise convergence/divergence behavior via choice of $f$" theme, but for a fixed classical node system rather than a constructed one. - erdos/1152 — OPEN; asks whether, for *any* fixed node sequence, some continuous $f$ forces near-best-degree polynomial interpolants to diverge almost everywhere — a "no array can be too good" negative-direction cousin of #671. - erdos/1153 — PROVED in 2026 by Terence Tao (arXiv:2603.21453), local Bernstein theory; the technically closest *fully verified, published* 2026 advance on Lebesgue-function lower bounds, and the most credible independent toolkit if the #671 Lean proof needs an alternative or corroborating construction. - concept/lebesgue-constant — the classical quantity $\Lambda^n=\max_x\lambda^n(x)$, $\lambda^n(x)=\sum_i|p_i^n(x)|$; Faber/Bernstein/Erdős's $\gg\log n$ lower bound and the Chebyshev-node $O(\log n)$ upper bound are the backdrop against which #671's *pointwise* blow-up question is posed. - concept/uniform-boundedness-principle — Banach–Steinhaus: unboundedness of $\lambda^n(x)$ at a point $x$ is precisely the condition under which the set of continuous $f$ with $\mathcal L^nf(x)\not\to f(x)$ is comeager (comeager, not "all" — the loophole #671 exploits). - concept/local-bernstein-theory — Tao's 2026 technique (arXiv:2603.21453) for localized exponential-type/Lebesgue-constant lower bounds via Nevanlinna's two-constants theorem; solved the adjacent erdos/1153. - concept/stagewise-cell-shrinking-array-construction — the claimed #671 proof's core device: countably many finite stages, each shrinking a family of disjoint "cells," alternately engineering a "collision-pair" row (forces local Lebesgue blow-up) and an "exterior" row (forces blow-up off the cells) while keeping "filler" rows stable, so the array is simultaneously everywhere-unbounded and pointwise-tameable. - concept/pigeonhole-nested-interval-selection — the claimed proof's mechanism for producing, given a fixed target $f$, a single convergence point $x_f$: at each stage pick whichever of two "close sample" nodes $f$ is nearer to, yielding nested shrinking cells with a unique common limit point. - concept/lz-string-url-sharing — practical technique: AI-generated Lean/code artifacts shared via live.lean-lang.org (or similar playgrounds) are embedded in the URL fragment as lz-string-compressed base64, retrievable and auditable offline by anyone (as done here) without needing a live browser session — relevant methodology for verifying *any* future "AI solved Erdős problem N" forum claim on this site.

PRIOR-ART SCAN (2026-07-03)

Verdict: ACTIVELY-WORKED — and, as of this scan, upgraded to independently machine-verified-by-us. Do not attempt a fresh derivation; the hard mathematical work already exists, is public, and we have now personally confirmed it type-checks. No fresh-derivation attack applies.

What's new since the 2026-07-02 entry above

The 2026-07-02 provenance note (in the frontmatter/body above) had decoded the claimed Lean proof but explicitly *could not compile it* ("no Mathlib toolchain available in this session"). This scan closes that gap:

1. Re-fetched erdosproblems.com/671 directly (curl -sS -L -H 'User-Agent: Mozilla/5.0 ...' https://www.erdosproblems.com/671, 2026-07-03). Confirmed verbatim: statement (both parts), OPEN status widget text, and, not previously flagged, an existing curated remark — Bernstein [Be31] proved every array has *some* point of Lebesgue blow-up, and Erdős–Vértesi [ErVe80] proved every array has *some* continuous $f$ diverging almost everywhere — i.e. the classical literature already shows both "some point blows up" and "some $f$ diverges everywhere" are unavoidable; #671 asks whether a *specific* $f$ can still dodge divergence at a *specific* blow-up point. Also confirmed: problem-status-widget shows data-current-status="claimed" = "A claimed solution has been posted in the comments" (i.e. even the site's own lightweight signal, distinct from the curated OPEN status, already flags this). 2. Re-fetched the forum thread (https://www.erdosproblems.com/forum/discuss/671, 2026-07-03): confirmed comment from user "Leeham" — "GPT Pro resolves both questions in the affirmative" — linking the same Overleaf writeup (https://www.overleaf.com/read/gqmfrhsprtqm#59ac11, still only client-rendered, text not extractable via curl or WebFetch) and the same live.lean-lang.org Lean artifact. 3. Re-fetched the teorth/erdosproblems AI-contributions wiki (raw.githubusercontent.com/wiki/teorth/erdosproblems/AI-contributions-to-Erdős-problems.md, snapshot "as of Jun 30, 2026", re-checked 2026-07-03): confirmed row [671] | Codex, GPT-5.5 Pro | 22 Jun, 2026 | ⚪ Candidate full solution (Lean) and the legend ⚪ = Unverified (vs 🟢 Full resolution, 🟡 Partial, 🔴 Incorrect). 4. Independently decoded the Lean artifact myself, from scratch (did not trust the previous decode): extracted the #codez= fragment from the raw forum HTML, percent-decoded it, ran it through the real lz-string npm package's decompressFromBase64. Recovered the identical 2829-line, 0-sorry Mathlib file, theorem erdos_671 with the type matching Part 2 verbatim. Spot-checked the core definitions against Erdős's actual notation: fundamental (built from Mathlib's Lagrange.basis, matches $p_i^n$ exactly via Lagrange.basisDivisor/product formula), interpolant = ∑ f(node i) * fundamental (matches $\mathcal L^nf$), lebesgue = ∑ |fundamental|$ (matches $\lambda^n$), structure Row (n) where ... node : ι ↪ Interval with Interval := Set.Icc (-1:ℝ) 1 and card_ι : Fintype.card ι = n (an *embedding* into $[-1,1]$, i.e. nodes are automatically distinct and in-range — matches the problem's implicit distinctness requirement). No red flags in this spot check. 5. **New this scan — actually compiled it.** Installed elan fresh, cloned leanprover-community/mathlib4 at its current master (lean-toolchain = leanprover/lean4:v4.32.0-rc1), ran lake exe cache get (downloaded all 8,617 prebuilt .olean files, no errors) and lake build Mathlib (8,632 jobs, Build completed successfully). Dropped the independently-decoded Lean source into the project root as Erdos671Check.lean and ran lake env lean Erdos671Check.lean. **Result: it elaborates with zero errors**, and the file's own trailing #print axioms erdos_671 line prints exactly: ` 'Erdos671.erdos_671' depends on axioms: [propext, Classical.choice, Quot.sound] ` — the three standard, harmless Lean/Mathlib axioms (no sorryAx, no custom/suspicious axiom, no native_decide). Also grepped the full source for axiom, opaque, native_decide, Lean.ofReduceBool, unsafe — none present. 6. **Checked for independent third-party verification/refutation elsewhere**: WebSearch for "erdos_671" Lean Mathlib, "Erdos problem 671" GPT-5.5 Pro Codex arXiv writeup, github "Erdos671" OR "erdos-671" Lean formalization — no arXiv writeup exists for #671 (unlike e.g. #728, which has arXiv:2601.07421, "Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof"), no HN/blog discussion, no independent repo. Checked the third-party community repo github.com/plby/lean-proofs (src/v4.24.0/ErdosProblems/, 91 files, via GitHub API), which mirrors verified Erdős-problem Lean proofs (has e.g. Erdos678.lean) — **no Erdos671.lean present**, confirming no independent party has verified/merged this yet. 7. **Spot-checked the "Related" cluster claims** (all re-fetched 2026-07-03, curl` with browser UA): erdos/1129 PROVED, erdos/1130 PROVED, erdos/1151 OPEN, erdos/1152 OPEN — all confirmed. erdos/1153 confirmed PROVED, "Additional thanks to: Wouter van Doorn and Terence Tao". arxiv.org/abs/2603.21453 fetched and confirmed to be Tao's "Local Bernstein theory, and lower bounds for Lebesgue constants," explicitly stated to "localize the Erdős lower bound" and answer "a question of Erdős and Turán" on Lebesgue constants — matches the citation.

Bottom line

- The claimed proof is real, public, sorry-free, and now independently confirmed by us to type-check against genuine current Mathlib, with a statement whose type matches Erdős's Part 2 (the stronger claim, which implies Part 1) and whose core definitions faithfully encode $p_i^n$, $\mathcal L^nf$, $\lambda^n$. - It is not yet reflected in erdosproblems.com's curated OPEN status (editorial lag — the site's own disclaimer says comment activity isn't auto-incorporated), not yet independently mirrored/confirmed by any third party we could find (not in plby/lean-proofs, no arXiv writeup, no external discussion), and the residual risk is exclusively statement-fidelity (does the Lean formalization capture Erdős's actual mathematical intent, as opposed to some subtly different but type-matching statement) — our spot-check of the core definitions found no discrepancy, but we did not read all ~2,800 lines line-by-line. - Action for us: do not attempt a fresh proof of #671 — it would be redundant. If there is future value here, it is in (a) writing up the informal argument for a human-readable note or arXiv-style writeup (nobody has done this yet, unlike #728), since that is the one thing the AI-contributions ecosystem is missing for this problem, or (b) a full line-by-line audit of the ~50 preliminary lemmas for statement-fidelity, which we did not exhaustively do. Neither is a "fresh derivation," so no concrete first experiment is given per the task's own criterion (only required for FRESH-AND-TRACTABLE verdicts).

Sources actually read (this scan)

- https://www.erdosproblems.com/671 (curl, browser UA) - https://www.erdosproblems.com/forum/discuss/671 (curl, browser UA) - https://raw.githubusercontent.com/wiki/teorth/erdosproblems/AI-contributions-to-Erd%C5%91s-problems.md - https://www.overleaf.com/read/gqmfrhsprtqm#59ac11 (WebFetch; confirmed client-rendered, no text extractable) - live.lean-lang.org share-link fragment embedded in the forum comment (decoded locally via lz-string npm package decompressFromBase64, independently reproduced) - https://github.com/plby/lean-proofs (GitHub API, contents of src/v4.24.0/ErdosProblems/) - https://www.erdosproblems.com/1129, /1130, /1151, /1152, /1153 (curl, browser UA) - https://arxiv.org/abs/2603.21453 (Tao, "Local Bernstein theory, and lower bounds for Lebesgue constants") - leanprover-community/mathlib4 @ current master (lean-toolchain: leanprover/lean4:v4.32.0-rc1), compiled locally via elan + lake exe cache get + lake build Mathlib + lake env lean on the decoded source