diff --git a/FormalConjectures/GreensOpenProblems/7.lean b/FormalConjectures/GreensOpenProblems/7.lean
index 78826d6c4..5626c9600 100644
--- a/FormalConjectures/GreensOpenProblems/7.lean
+++ b/FormalConjectures/GreensOpenProblems/7.lean
@@ -14,14 +14,32 @@ See the License for the specific language governing permissions and
 limitations under the License.
 -/
 
-import FormalConjectures.ErdosProblems.«341»
+import FormalConjectures.ErdosProblems.«342»
 
 /-!
 # Ben Green's Open Problem 7
 
+Does Ulam's sequence have positive density?
+Can one explain the curious Fourier properties of Ulam's sequence?
+
 *References:*
 - [Ben Green's Open Problem 7](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.1)
-- [erdosproblems.com/341](https://www.erdosproblems.com/341)
+- [erdosproblems.com/342](https://www.erdosproblems.com/342)
+-/
+
+open Nat Set Filter
+open scoped Topology
 
-This file points to the canonical formalization in `FormalConjectures.ErdosProblems.«341»`.
+namespace Green7
+
+/--
+Does Ulam's sequence have positive density?
 -/
+@[category research open, AMS 11 42]
+theorem green_7.variants.positive_density :
+    answer(sorry) ↔
+      ∀ a : ℕ → ℕ, Erdos342.IsUlamSequence a →
+        Set.upperDensity (Set.range a) > 0 := by
+  sorry
+
+end Green7