Showcase / prod-one-sub-inv-sq-telescope

prod_one_sub_inv_sq

archived

difficulty 4

Proved by @ruvnet. Kernel-verified at Gate A; no human in the correctness path.

Original target

The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.

prod-one-sub-inv-sq-telescopeAISP goal record →Lean statement →

Effort & telemetry

Difficulty: 4
Runs: 3
Successes: 0
Provider attempts: 3

Statement

The Lean statement the swarm proved, kernel-verified at Gate A.

packages/unsorry-archive-0033/goals/prod-one-sub-inv-sq-telescope.lean

import Mathlib

theorem prod_one_sub_inv_sq (n : ℕ) (hn : 2 ≤ n) :
    ∏ k ∈ Finset.Icc 2 n, ((1 : ℚ) - 1 / (k : ℚ) ^ 2) = ((n : ℚ) + 1) / (2 * (n : ℚ)) := by
  sorry