Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1975P3

module

public import Mathlib.Algebra.EuclideanDomain.Basic
public import Mathlib.Algebra.EuclideanDomain.Field
public import Mathlib.Algebra.Polynomial.BigOperators
public import Mathlib.Algebra.Polynomial.RingDivision
public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Data.Nat.Factorial.BigOperators
public import Mathlib.RingTheory.Coprime.Lemmas
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.Positivity.Basic
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1975, Problem 3

A polynomial p(x) of degree n satisfies p(0) = 0, p(1) = 1/2, p(2) = 2/3, ... ,
p(n) = n/(n+1). Find p(n+1).
-/

namespace Usa1975P3

open Polynomial

noncomputable /- determine -/ abbrev answer (n : ℕ) : ℝ := sorry

theorem usa1975_p3 (n : ℕ) (p : ℝ[X]) (hp : p.natDegree = n)
    (h : ∀ k ∈ Finset.range (n + 1), p.eval (k : ℝ) = (k : ℝ) / (k + 1)) :
    p.eval ((n : ℝ) + 1) = answer n := sorry

end Usa1975P3

File author(s): Kimi K3

This problem has a complete formalized solution.