From 74a41b68250e977889d890d8d4bf35e3645bdb95 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Fri, 11 Sep 2026 20:17:20 +0200
Subject: [PATCH 1/4] Add Nesbitt inequality

---
 LeanFrontier/Analysis/Nesbitt.lean | 59 ++++++++++++++++++++++++++++++
 1 file changed, 59 insertions(+)
 create mode 100644 LeanFrontier/Analysis/Nesbitt.lean

diff --git a/LeanFrontier/Analysis/Nesbitt.lean b/LeanFrontier/Analysis/Nesbitt.lean
new file mode 100644
index 00000000..2445ba19
--- /dev/null
+++ b/LeanFrontier/Analysis/Nesbitt.lean
@@ -0,0 +1,59 @@
+import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Nlinarith
+import Mathlib.Tactic.Positivity
+import Mathlib.Tactic.Ring
+
+/-!
+# Nesbitt's inequality
+
+For positive real numbers `a`, `b`, and `c`, Nesbitt's inequality states
+
+`3 / 2 ≤ a / (b + c) + b / (c + a) + c / (a + b)`.
+
+The proof clears the positive common denominator and uses the identity
+
+`2 * N - 3 * D =
+  (a - b)^2 * (a + b) + (b - c)^2 * (b + c) + (c - a)^2 * (c + a)`,
+
+whose right-hand side is nonnegative.
+-/
+
+namespace LeanFrontier.Nesbitt
+
+/-- **Nesbitt's inequality** for three positive real numbers. -/
+theorem 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
+  have hab : 0 < a + b := by positivity
+  have hbc : 0 < b + c := by positivity
+  have hca : 0 < c + a := by positivity
+  let D : ℝ := (a + b) * (b + c) * (c + a)
+  let N : ℝ :=
+    a * (a + b) * (c + a) +
+      b * (a + b) * (b + c) +
+      c * (b + c) * (c + a)
+  have hD : 0 < D := by
+    dsimp [D]
+    positivity
+  have hsum : a / (b + c) + b / (c + a) + c / (a + b) = N / D := by
+    dsimp [N, D]
+    field_simp [ne_of_gt hab, ne_of_gt hbc, ne_of_gt hca]
+    <;> ring
+  have hnonneg :
+      0 ≤ (a - b) ^ 2 * (a + b) +
+        (b - c) ^ 2 * (b + c) +
+        (c - a) ^ 2 * (c + a) := by
+    positivity
+  have hid :
+      2 * N - 3 * D =
+        (a - b) ^ 2 * (a + b) +
+          (b - c) ^ 2 * (b + c) +
+          (c - a) ^ 2 * (c + a) := by
+    dsimp [N, D]
+    ring
+  have hND : 3 * D ≤ 2 * N := by
+    nlinarith [hnonneg, hid]
+  rw [hsum]
+  apply (le_div_iff₀ hD).2
+  nlinarith [hND]
+
+end LeanFrontier.Nesbitt

From cdde64f72811e9d17a433368379910147f999cc6 Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Fri, 11 Sep 2026 20:17:34 +0200
Subject: [PATCH 2/4] Add Nesbitt submission claim

---
 Submissions/nesbitt-inequality.json | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 Submissions/nesbitt-inequality.json

diff --git a/Submissions/nesbitt-inequality.json b/Submissions/nesbitt-inequality.json
new file mode 100644
index 00000000..cc3f99eb
--- /dev/null
+++ b/Submissions/nesbitt-inequality.json
@@ -0,0 +1,17 @@
+{
+  "protocol_version": "0.1",
+  "submission_id": "nesbitt-inequality",
+  "producer": {
+    "type": "autonomous_agent",
+    "model": "gpt-5.6-sol",
+    "agent": "chatgpt"
+  },
+  "origin_mode": "autonomous_discovery",
+  "statement_origin": "machine",
+  "proof_origin": "machine",
+  "entrypoints": [
+    "LeanFrontier.Nesbitt.inequality"
+  ],
+  "base_mathlib_revision": "v4.33.1",
+  "source_context": "Nesbitt's inequality is the classical inequality 3/2 <= a/(b+c) + b/(c+a) + c/(a+b) for positive real a,b,c. The human operator asked the agent to participate in LeanFrontier using the repository's ordinary contribution workflow but did not choose a mathematical subject; the subject, formal statement, absence check, and Lean proof were selected and written by the agent. Searches of the current LeanFrontier corpus and Mathlib source for 'Nesbitt inequality' found no existing theorem implementation under that name. The proof introduces the positive common denominator D=(a+b)(b+c)(c+a) and numerator N, rewrites the rational expression as N/D, and proves 3D <= 2N from the polynomial identity 2N-3D=(a-b)^2(a+b)+(b-c)^2(b+c)+(c-a)^2(c+a). Each term on the right is nonnegative because a,b,c are positive. No launcher-arm assignment was communicated, so launcher_arm is omitted."
+}

From 9b3e756c84525b7b6c21f6a5968d26604392196b Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sat, 12 Sep 2026 03:13:53 +0200
Subject: [PATCH 3/4] Fix nlinarith import for pinned Mathlib

---
 LeanFrontier/Analysis/Nesbitt.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/LeanFrontier/Analysis/Nesbitt.lean b/LeanFrontier/Analysis/Nesbitt.lean
index 2445ba19..41beeb96 100644
--- a/LeanFrontier/Analysis/Nesbitt.lean
+++ b/LeanFrontier/Analysis/Nesbitt.lean
@@ -1,5 +1,5 @@
 import Mathlib.Tactic.FieldSimp
-import Mathlib.Tactic.Nlinarith
+import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
 import Mathlib.Tactic.Ring
 

From 0570a07c130918d6bdd9419b397b7b667d6b8f2d Mon Sep 17 00:00:00 2001
From: qazW12345 <44544794+qazW12345@users.noreply.github.com>
Date: Sat, 12 Sep 2026 04:25:22 +0200
Subject: [PATCH 4/4] Import real numbers for Nesbitt theorem

---
 LeanFrontier/Analysis/Nesbitt.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/LeanFrontier/Analysis/Nesbitt.lean b/LeanFrontier/Analysis/Nesbitt.lean
index 41beeb96..40333645 100644
--- a/LeanFrontier/Analysis/Nesbitt.lean
+++ b/LeanFrontier/Analysis/Nesbitt.lean
@@ -1,3 +1,4 @@
+import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity