lean_workbook_plus_21667

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find a polynomial $P(x)$ with real coefficients, such that $P(n)=2^n$ for all $n=0,1,2,...,9$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21667 (x : ℝ) : ∃ P : ℝ → ℝ, (∀ n : ℕ, n < 10 → P n = 2 ^ n)   :=  by sorry

Source