Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. With the Lebesgue function of the th row of nodes and the Lagrange interpolant, the write-up constructs a node system with for every such that every continuous has a point with , which answers both questions of Problem 671 yes. As the tab entry describes it, the construction runs in stages on nested protective intervals. On each interval a family of rows indexed by pairs contains coalescing nodes whose three principal Lagrange coefficients approach , and , so the Lebesgue function of such a row is at least there, while the rows not selected keep their Lebesgue functions locally at most ; a separate exterior row makes the Lebesgue function large outside the stage intervals, and nesting gives unbounded Lebesgue functions at every point. For a fixed continuous , stage offers cluster values, so two of them have -values within of each other; choosing the row indexed by that pair and taking bounds the interpolation error by , which tends to zero. The entry's notes say that the write-up re-derives the whole argument of Price's claim and reduces its stage sample count from to , that it is intended as an independent verification and quantitative refinement of that claim, and that it claims no priority for the coalescing-node construction; the submitter adds that the moderators may treat it as a verification rather than a separate claim. The claimant is the forum user QuietMethod, who declares assistance from the AI system named as OpenAI Codex (GPT-5) in developing, checking and formalizing the argument.
Submission note. Posted to erdosproblems.com as a proof claim by QuietMethod (account quietmethod) on 24 July 2026, giving "OpenAI Codex (GPT-5)" as the AI used:
This claim answers both questions affirmatively. The construction proceeds in stages using nested protective intervals. On each interval, pair-indexed interpolation rows contain coalescing nodes whose three principal Lagrange coefficients approach A, -A, and 1. This makes the corresponding Lebesgue function at least A, while the Lebesgue functions of the non-selected rows remain locally bounded by 2. A separate exterior row makes the Lebesgue function large outside the stage intervals. The nested construction therefore gives limsup_{n -> infinity} lambda_n(x) = infinity for every x in [-1,1]. For a fixed continuous function f, at stage k we consider N_k = k^2 + 1 cluster values. The pigeonhole principle gives a pair whose f-values differ by at most 2||f||_infinity/k^2. Choosing the branch indexed by this pair and taking A_k = k gives an interpolation-error bound 3||f||_infinity/k + omega_f(1/k), which tends to zero. On all remaining rows, the Lebesgue function is at most Notes: This submission is intended as an independent verification and quantitative refinement of Liam Price's existing proof claim. It does not claim priority for the core coalescing-node construction. The writeup re-derives the full argument and reduces the stage sample count from k^3 + 1 to k^2 + 1. A corresponding Lean formalisation was checked with Lean 4.33.0-rc1 and mathlib. It contains no sorry, admit, or custom axioms; #print axioms reports only propext, Classical.choice, and Quot.sound. AI assistance from OpenAI Codex (GPT-5) was used in developing, checking, and formalising the argument. I welcome expert review. If the moderators consider the overlap with the existing claim too large for a separate proof claim, this may instead be treated as an independent verification and refinement. Project page with the proof summary, attribution, verification information, and public files: https://quietmethod-erdos671.gintsuta-kobo.chatgpt.site/
Standing. The claim was filed on the site's proof-claims tab on 24 July
2026 as a full proof, with no comments. The site's label is OPEN with the
page last edited 23 January 2026, before the claim, and its commentary does
not mention it. No refereed publication and no outside review was found.
The notes report a Lean formalization checked with Lean 4 and Mathlib, with
no sorry, admit or custom axiom and an axiom report of propext,
Classical.choice and Quot.sound; this corpus has not built it, so the
self-report gives no formalized evidence. The claim stays claimed.
Depends on. Nothing beyond the cited write-up, which re-derives the argument it refines rather than citing it as a premise.