diff --git a/FormalConjectures/ErdosProblems/289.lean b/FormalConjectures/ErdosProblems/289.lean
index 957b219d1..09d16b2d0 100644
--- a/FormalConjectures/ErdosProblems/289.lean
+++ b/FormalConjectures/ErdosProblems/289.lean
@@ -33,9 +33,10 @@ $$
 -/
 @[category research open, AMS 11]
 theorem erdos_289 : answer(sorry) ↔
-    (∀ᶠ k : ℕ in atTop, ∃ I : Fin k → Finset ℕ,
-      (∀ i, 2 ≤ #(I i) ∧ ∃ a b, 0 < a ∧ I i = Finset.Icc a b) ∧
-      ∑ i, ∑ n ∈ I i, (n⁻¹ : ℚ) = 1) := by
+    (∀ᶠ k : ℕ in atTop, ∃ I : Fin k → ℕ × ℕ,
+    (∀ i, (I i).1 < (I i).2) ∧
+    (∀ i j, i ≠ j → (I i).2 < (I j).1 ∨ (I j).2 < (I i).1) ∧
+    ∑ i, ∑ n ∈ .Icc (I i).1 (I i).2, (n⁻¹ : ℚ) = 1) := by
   sorry
 
 end Erdos289