Showcase / nesbitt-inequality

nesbitt_inequality

archived

difficulty 4

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

nesbitt-inequalityAISP 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-0033/goals/nesbitt-inequality.lean

import Mathlib

theorem nesbitt_inequality (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    3 / 2 ≤ a / (b + c) + b / (c + a) + c / (a + b) := by
  sorry