Source labels openChecked July 26, 2026

Erdős Problem 1133

Let $C>0$ . There exists $\epsilon>0$ such that if $n$ is sufficiently large the following holds.

Mathematical statement

Let $C>0$ . There exists $\epsilon>0$ such that if $n$ is sufficiently large the following holds.

For any $x_1,\ldots,x_n\in [-1,1]$ there exist $y_1,\ldots,y_n\in [-1,1]$ such that, if $P$ is a polynomial of degree $m<(1+\epsilon)n$ with $P(x_i)=y_i$ for at least $(1-\epsilon)n$ many $1\leq i\leq n$ , then $\max_{x\in [-1,1]}\lvert P(x)\rvert >C.$

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_1133

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_1133 :    answer(sorry) ↔    ∀ C > (0 : ℝ), ∃ ε > (0 : ℝ), ∀ᶠ n : ℕ in atTop,      ∀ x : Fin n → Icc (-1 : ℝ) 1,        ∃ y : Fin n → Icc (-1 : ℝ) 1,          ∀ P : Polynomial ℝ,            (P.natDegree : ℝ) < (1 + ε) * (n : ℝ) →            ((Finset.univ.filter (fun i ↦ P.eval (x i : ℝ) = (y i : ℝ))).card : ℝ) ≥              (1 - ε) * (n : ℝ) →            ∃ z ∈ Icc (-1 : ℝ) 1, |P.eval z| > C := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/1133background