putnam-v1 / putnam-1967-a6

putnam-1967-a6

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal putnam-1967-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-1967-a6.lean

import Mathlib

open Nat Topology Filter
abbrev putnam_1967_a6_solution : ℕ := 8

theorem putnam_1967_a6 (abneq0 : (Fin 4 → ℝ) → (Fin 4 → ℝ) → Prop)
(habneq0 : abneq0 = (fun a b : Fin 4 → ℝ => a 0 * b 1 - a 1 * b 0 ≠ 0))
(numtuples : (Fin 4 → ℝ) → (Fin 4 → ℝ) → ℕ)
(hnumtuples : ∀ a b : Fin 4 → ℝ, numtuples a b = {s : Fin 4 → ℝ | ∃ x : Fin 4 → ℝ, (∀ i : Fin 4, x i ≠ 0) ∧ (∑ i : Fin 4, a i * x i) = 0 ∧ (∑ i : Fin 4, b i * x i) = 0 ∧ (∀ i : Fin 4, s i = Real.sign (x i))}.encard)
: (∃ a b : Fin 4 → ℝ, abneq0 a b ∧ numtuples a b = putnam_1967_a6_solution) ∧ (∀ a b : Fin 4 → ℝ, abneq0 a b → numtuples a b ≤ putnam_1967_a6_solution) := by
  sorry

Runs (0)

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