Erdős Problem #1151
Erdős problem #1151 · erdosproblems.com/1151
Let be the Lagrange interpolation polynomials of a continuous on the Chebyshev nodes. Prove that, for any closed , there exists a continuous function such that is the set of limit points of .
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI co-developed
- Method
- Construction
- Field
- Analysis, Polynomials
- Posed by
- Paul Erdős
- Year posed
- 1999
- Years open
- 27y
- Solved
- 2026-04-30
- Model
- GPT-5.5 Pro, Codex
- Vendor
- OpenAI
- Collaborators
- Przemysław Chojecki, Allen Hart
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
An elementary solution via a primitive-row decomposition of the Chebyshev-node measures; the main theorem is formalized in Lean, but erdosproblems.com still lists the problem open
What the AI did
The solution was obtained with GPT-5.5 Pro using an explicit primitive-row decomposition of the Chebyshev-node measures; Theorem 1.1(a), the main contribution, was subsequently formalized largely autonomously by ChatGPT and Codex.
Verification
Theorem 1.1(a), the main part of the contribution, is formalized in Lean and the formalization was confirmed correct on the forum; part (b) is unformalized because it depends on an Erdős result absent from mathlib. erdosproblems.com still lists the problem open.