putnam-v1 / putnam-1965-a6

putnam-1965-a6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1965-a6

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-1965-a6.lean

import Mathlib

open EuclideanGeometry Topology Filter Complex

theorem putnam_1965_a6 (u v m : ℝ)
    (hu : 0 < u)
    (hv : 0 < v)
    (hm : 1 < m) :
    (∃ᵉ (x > 0) (y > 0),
      u * x + v * y = 1 ∧
      x ^ m + y ^ m = 1 ∧
      u = x ^ (m - 1) ∧
      v = y ^ (m - 1)) ↔
    ∃ n, u ^ n + v ^ n = 1 ∧ m⁻¹ + n⁻¹ = 1 := by
  sorry

Runs (0)

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