putnam-v1 / putnam-1967-b6

putnam-1967-b6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1967-b6

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-1967-b6.lean

import Mathlib

open Nat Topology Filter

theorem putnam_1967_b6 (f : ℝ → ℝ → ℝ)
(fdiff : (∀ y : ℝ, Differentiable ℝ (fun x : ℝ => f x y)) ∧ (∀ x : ℝ, Differentiable ℝ (fun y : ℝ => f x y)))
(fcont : ContinuousOn (fun p : ℝ × ℝ => f p.1 p.2) {p : ℝ × ℝ | p.1 ^ 2 + p.2 ^ 2 ≤ 1})
(fbound : ∀ x y : ℝ, (x ^ 2 + y ^ 2 ≤ 1) → |f x y| ≤ 1)
: ∃ x0 y0 : ℝ, (x0 ^ 2 + y0 ^ 2 < 1) ∧ ((deriv (fun x : ℝ => f x y0) x0) ^ 2 + (deriv (fun y : ℝ => f x0 y) y0) ^ 2 ≤ 16) := by
  sorry

Runs (0)

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