putnam-v1 / putnam-1963-a3

putnam-1963-a3

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1963-a3

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/putnam-1963-a3.lean

import Mathlib

open Nat Set Topology Filter
noncomputable abbrev putnam_1963_a3_solution : (ℝ → ℝ) → ℕ → ℝ → ℝ → ℝ := fun (f : ℝ → ℝ) (n : ℕ) (x : ℝ) (t : ℝ) ↦ (x - t) ^ (n - 1) * (f t) / ((n - 1)! * t ^ n)

theorem putnam_1963_a3 (P : ℕ → (ℝ → ℝ) → (ℝ → ℝ))
    (hP : P 0 = id ∧ ∀ i y, P (i + 1) y = P i (fun x ↦ x * deriv y x - i * y x))
    (n : ℕ)
    (hn : 0 < n)
    (f y : ℝ → ℝ)
    (hf : ContinuousOn f (Ici 1))
    (hy : ContDiffOn ℝ n y (Ici 1))
    (hy1 : ContDiffAt ℝ n y 1) :
    (∀ i < n, deriv^[i] y 1 = 0) ∧ (Ici 1).EqOn (P n y) f ↔
    ∀ x ≥ 1, y x = ∫ t in (1 : ℝ)..x, putnam_1963_a3_solution f n x t := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.