Showcase / descartes-total-angular-defect

descartes_total_angular_defect

archived

difficulty 4

Proved by @perttu. 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.

descartes-total-angular-defectAISP goal record →Lean statement →

Effort & telemetry

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

Statement

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

packages/unsorry-archive-0004/goals/descartes-total-angular-defect.lean

import Mathlib

theorem descartes_total_angular_defect (p q V E F : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q)
    (hV : 0 < V) (hF : 0 < F) (h1 : p * F = 2 * E) (h2 : q * V = 2 * E) (h3 : V + F = E + 2) :
    (V : ℝ) * (2 * Real.pi - (q : ℝ) * (((p : ℝ) - 2) / (p : ℝ)) * Real.pi) = 4 * Real.pi := by
  sorry