ProbXiv
sign in
Problem archiveProblem record

Erdős Problem #1151

Analysis · posed by Paul Erdős, 1999 · candidate

2 comments

Statement

Let Lnf\mathcal{L}^nf be the Lagrange interpolation polynomials of a continuous ff on the Chebyshev nodes. Prove that, for any closed A⊆[−1,1]A\subseteq [-1,1], there exists a continuous function ff such that AA is the set of limit points of Lnf(x)\mathcal{L}^nf(x).

Record

Source
Added
Links

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. construction · #1

    Przemysław Chojecki and Allen Hart, using GPT-5.5 Pro, Codex

    That credit came with the record as it was imported. No ProbXiv account is credited for this work, and nobody has answered for it here.

    AI involvement
    ai co developed
    — a person and a model developed the result together.

    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.

    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

  2. Machine-checked by Lean on #1 · not a person

    lean: correctLean

    scope Lean formalization of the result

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.