From e83ba8f786c187329578e43edb47c9372b98db6d Mon Sep 17 00:00:00 2001
From: Aleksandr_NFA <sanexxx777@gmail.com>
Date: Fri, 3 Jul 2026 08:34:46 +1000
Subject: [PATCH] feat(ErdosProblems/888): record order of growth (semiprimes +
 matching upper bound)

---
 FormalConjectures/ErdosProblems/888.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/FormalConjectures/ErdosProblems/888.lean b/FormalConjectures/ErdosProblems/888.lean
index 674ee1e105..edc6c6a3ca 100644
--- a/FormalConjectures/ErdosProblems/888.lean
+++ b/FormalConjectures/ErdosProblems/888.lean
@@ -20,6 +20,14 @@ import FormalConjectures.Util.ProblemImports
 # Erdős Problem 888
 
 *Reference:* [erdosproblems.com/888](https://www.erdosproblems.com/888)
+
+Let $f(n)$ be the size of the largest $A \subseteq \{1,\dots,n\}$ with $ad = bc$ whenever
+$a \le b \le c \le d \in A$ and $abcd$ is a perfect square. The order of growth was determined
+in 2026: the semiprimes (noted by Cambie and Weisenberg) give
+$f(n) \ge (1 + o(1)) \frac{n \log\log n}{\log n}$, and a matching upper bound
+$f(n) \ll \frac{n \log\log n}{\log n}$ was proved by GPT-5.5 Pro (prompted by Chojecki),
+so $f(n) = \Theta\!\left(\frac{n \log\log n}{\log n}\right)$. The exact value of $f(n)$
+remains open.
 -/
 
 open Classical Filter
@@ -53,3 +61,19 @@ theorem erdos_888.variants.sarkozy : (fun n ↦ (Nat.findGreatest (p n) n : ℝ)
 @[category research solved, AMS 11]
 theorem erdos_888.variants.primes : (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ )) ≫ (fun n : ℕ ↦ n / (n : ℝ).log) := by
   sorry
+
+/-- The **semiprimes** $\le n$ satisfy the condition, and there are
+$(1 + o(1)) \frac{n \log\log n}{\log n}$ of them, giving the sharp lower bound.
+Noted by Cambie and Weisenberg. -/
+@[category research solved, AMS 11]
+theorem erdos_888.variants.semiprimes :
+    (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ)) ≫ (fun n : ℕ ↦ n * (n : ℝ).log.log / (n : ℝ).log) := by
+  sorry
+
+/-- **Matching upper bound** (proved by GPT-5.5 Pro, prompted by Chojecki, 2026):
+$f(n) \ll \frac{n \log\log n}{\log n}$. Together with `semiprimes` this determines
+the order of growth of $f(n)$. -/
+@[category research solved, AMS 11]
+theorem erdos_888.variants.upper_bound :
+    (fun n : ℕ ↦ (Nat.findGreatest (p n) n : ℝ)) ≪ (fun n : ℕ ↦ n * (n : ℝ).log.log / (n : ℝ).log) := by
+  sorry