---

Claim. For every fixed $-1\le a<b\le1$ and every $\varepsilon>0$ there is $N$ such that for every $n\ge N$ and every choice of $n$ distinct nodes in $[-1,1]$ some $t\in[a,b]$ has $\lambda(t)>(2/\pi-\varepsilon)\log n$, where $\lambda$ is the Lebesgue function; this is the question of Problem 1153 with the $o(1)$ read as an arbitrary fixed $\varepsilon$ and a threshold uniform over the nodes. The claimant, Ethan Yang, registered it on the site's proof-claims page on 2026-08-31 as an alternative proof, after the resolution of Tao 2026; the site's claim line records that GPT-5.6 Sol was used. The claim consists of a written argument and a Lean 4 development in one repository, whose only commit, of 2026-08-31, is pinned above. The repository's own description,: a final theorem Erdos1153.erdos1153_main of the type Erdos1153.Target, 69 Lean files and 26,525 lines against Lean 4.27.0 and Mathlib 4.27.0, a statement file, a clause-by-clause correspondence table, a statement audit proving the maximum formulation equivalent to the witness formulation, an expected axiom report of propext, Classical.choice and Quot.sound, and a verification script run by continuous integration. The table says that the development proves the $\varepsilon$ form and does not claim Tao's additive $O(1)$ remainder, and names the interpretive choices that kernel checking cannot settle: distinct nodes, the natural logarithm, and the threshold placed before the node family. The development was released under the MIT license.

Submission note. Posted to erdosproblems.com as a proof claim by Ethan Yang (account EthanYang) on 31 August 2026, giving "GPT-5.6 Sol" as the AI used:

I give an alternative proof of Erdős Problem #1153. For every fixed -1 <= a < b <= 1 and every epsilon > 0, uniformly over all choices of n distinct interpolation nodes in [-1,1], the proof shows that for all sufficiently large n, max_{x in [a,b]} lambda(x) > (2/pi - epsilon) log n. The main localization step uses the de Boor--Pinkus gap-height comparison theory. A collapse argument shows that any consecutive block of m nodes contains an intervening gap whose Lebesgue-function maximum is at least the common gap height of an optimal equioscillating m-node configuration. A fixed-interval damping/Remez argument then gives a sparse--dense dichotomy: either the chosen interior interval contains a positive proportion of all nodes, in which case the consecutive-block result applies, or the Lebesgue function there is already exponentially large. The sharp 2/pi coefficient comes from a full-interval estimate proved via a clipped arcsine pair-energy argument. Notes: This is an alternative proof of an already resolved problem and is not a claim of priority for its original resolution. The accompanying Lean 4/Mathlib development gives a complete formal proof. The de Boor--Pinkus comparison theorem and sharp full-interval estimate are proved within the development. The verification workflow rejects 'sorry' and project-defined axioms; '#print axioms' reports only 'propext', 'Classical.choice', and 'Quot.sound'. To my knowledge, #1153 had no previous public Lean formalisation. I would particularly welcome independent checking that the formal target faithfully captures the original problem's quantifiers and asymptotic interpretation.

Argument. In the written outline the proof has four parts. First, a sharp bound on the whole interval: a pair energy, summing over pairs of nodes the geometric mean of a clipped arcsine weight at the two nodes divided by their distance, is bounded below by about $(1/\pi)n^2\log n$ through a partition of $[-1,1]$ into geometric bins in the arcsine coordinate, and bounded above by $n(n-1)/2$ times the Lebesgue constant through signed combinations of the fundamental polynomials and a weighted Bernstein inequality derived from a finite Riesz interpolation formula; the two bounds give $\max_{[-1,1]}\lambda>(2/\pi-\varepsilon)\log n$ uniformly in the nodes. Second, the development reproves the comparison theorem of de Boor and Pinkus 1978 for arrays with fixed endpoints: a unique array equalizes the gap maxima, and an array whose gap maxima are all at most those of another array equals it. Third, a localization step: in any consecutive block of $m$ nodes some internal gap carries a maximum at least the common height of the equioscillating $m$-node array, shown by collapsing the block onto a small affine copy of that array and applying the comparison theorem. Fourth, a dichotomy on nested fixed intervals $J_0\subset J_1\subset[a,b]$: if few nodes lie in $J_1$, a polynomial vanishing at them and damped away from a point of $J_0$ forces $\lambda$ to be exponentially large there; otherwise a positive proportion $m\ge cn$ of the nodes forms a consecutive block in $J_1$, and the localization with the sharp bound gives $\lambda(t)>(2/\pi-\varepsilon/2)\log m$ at a point $t\in[a,b]$, where $\log m\ge\log n-O(1)$. The site's statement is then recovered by sorting an arbitrary enumeration of the nodes, which leaves $\lambda$ unchanged.

Standing. The site registers the claim with its standard notice that it gives no correctness guarantee and that its associates have not examined any part; the thread had no comments (accessed 2026-10-07), and the site's label credits Tao. No independent review, acceptance by the site's curator, or refereed write-up is recorded. No build of the development, printout of its axioms or audit of its statement by this corpus is recorded; the description above is the repository's own, so no evidence is listed and the problem's standing rests on the accepted claim alone.

Depends on. Nothing in this wiki; the link to the de Boor and Pinkus page is context for the comparison theorem the development reproves.