Erdős Problem 1152: Polynomial Interpolation and Non-Convergence

### What is the conjecture

For each $n \geq 1$, fix a sequence of $n$ distinct numbers $x_{1n}, x_{2n}, \ldots, x_{nn} \in [-1,1]$. Let $\epsilon = \epsilon(n) \to 0$ as $n \to \infty$.

**Problem:** Does there exist a continuous function $f:[-1,1] \to \mathbb{R}$ such that for the unique sequence of interpolating polynomials $p_n$ satisfying $\deg p_n < (1+\epsilon(n))n$ and $p_n(x_{kn}) = f(x_{kn})$ for all $1 \leq k \leq n$, the convergence $p_n(x) \to f(x)$ fails for almost every $x \in [-1,1]$?

This problem contrasts with a theorem of Erdős, Kroó, and Szabados: when $\epsilon > 0$ is fixed (independent of $n$), there always exist choices of nodes for which interpolating polynomials of degree less than $(1+\epsilon)n$ converge uniformly to any continuous function on $[-1,1]$. The open question asks whether this uniform convergence result breaks down when the "degree slack" parameter $\epsilon(n)$ vanishes.

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

**Sources:**
- https://www.erdosproblems.com/1152

### Prerequisites needed

**Formalizability Rating:** 2/5 (0 is best) (as of 2026-02-01)

Building blocks (1-3; from search results):
- `Polynomial` (univariate polynomials over ℝ)
- `ContinuousOn` (continuous functions on closed intervals)
- `Set.ImmediatelyMeasurable` / measure theory for "almost everywhere" convergence

Missing pieces (exactly 2; unclear/absent from search results):
- Formalization of finite point sets and interpolation conditions (exists in Mathlib but may need adaptation for this specific node configuration setup)
- Measure-theoretic formulation of non-convergence on a set of full measure (measure theory exists in Mathlib; connecting to pointwise convergence requires care)

Rating justification (1-2 sentences): The basic mathematical objects—polynomials, continuous functions, and measure theory—are all present in Mathlib. However, formalizing the existential quantifier over continuous functions and the interaction between degree constraints, interpolation conditions, and almost-everywhere non-convergence requires careful setup of the node configuration and measure-theoretic statement, making this moderately complex to state formally.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-41
* ams-40
* ams-28

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)