Erdős Problem 1151: Chebyshev Nodes and Lagrange Interpolation Divergence

### What is the conjecture

Let $a_1, \ldots, a_n$ be the Chebyshev nodes on $[-1, 1]$, i.e., the roots of the Chebyshev polynomial of the first kind. For a continuous function $f: [-1, 1] \to \mathbb{R}$, let $\mathcal{L}^n f(x)$ denote the Lagrange interpolation polynomial of degree $n-1$ that agrees with $f$ at the Chebyshev nodes:
$$\mathcal{L}^n f(x) = \sum_{i=1}^{n} f(a_i) \ell_i(x)$$
where $\ell_i(x)$ are the Lagrange basis polynomials.

**Conjecture**: For any closed set $A \subseteq [-1, 1]$, there exists a continuous function $f: [-1, 1] \to \mathbb{R}$ such that the set of all limit points of the sequence $\{\mathcal{L}^n f(x)\}_{n=1}^{\infty}$ is precisely the set $A$.

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

**Sources:**
- https://www.erdosproblems.com/1151 | Va99: Vargas (1999) - referenced as [Va99, 2.41] in original problem statement

### Prerequisites needed

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

Building blocks (1-3; from search results):
- Polynomial types and Lagrange basis construction (standard in Mathlib for polynomial rings)
- Continuous functions and closed sets on $[-1, 1]$ (topology and continuous maps are well-developed)
- Convergence and limit points of sequences in metric spaces (real analysis foundations)

Missing pieces (exactly 2; unclear/absent from search results):
- Definition of Chebyshev nodes as roots of Chebyshev polynomials and their properties (specific to approximation theory)
- Formalization of the limit set of a sequence of functions: for each $x$, the set of cluster points of $\{\mathcal{L}^n f(x)\}_{n \geq 1}$

Rating justification (1-2 sentences): The statement involves standard topology and continuous functions that exist in Mathlib, but requires new definitions of Chebyshev nodes and the limit-set construction for sequences of polynomials. Moderate additional work is needed to set up the approximation-theoretic context.

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

* ams-41
* ams-26

### 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)