From 0bce5ffd97e15a8ce28436fd598cddc4e6fa9dc8 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Mon, 2 Mar 2026 08:32:52 -0800 Subject: [PATCH 01/10] * Description > With a1=1 and a2=2 let a_{n+1} for n >= 2 be the least integer greater than a_n which can be expressed uniquely as a_i + a_j for i < j <= n. Do infinitely many pairs (a,a+2) occur in the sequence? - First part of Erdos 342, google-deepmind#2120 * Testing - Compiles successfully ```shell $ lake build FormalConjectures/ErdosProblems/342.lean Build completed successfully. ``` --- FormalConjectures/ErdosProblems/342.lean | 61 ++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 FormalConjectures/ErdosProblems/342.lean diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean new file mode 100644 index 000000000..965ab4550 --- /dev/null +++ b/FormalConjectures/ErdosProblems/342.lean @@ -0,0 +1,61 @@ +/- +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. +-/ +import FormalConjectures.Util.ProblemImports + +/-! +# Erdos Problem 342 + +*References:* +- [erdosproblems.com/342](https://www.erdosproblems.com/342) +- [OEIS A002858](https://oeis.org/A002858) +-/ + +namespace Ulam + +/-- +`UniqueUlamSum u n m` means that `m` has a unique representation as `u i + u j` +with `1 ≤ i < j ≤ n`. +-/ +def UniqueUlamSum (u : ℕ → ℕ) (n m : ℕ) : Prop := + ∃! ij : ℕ × ℕ, + 1 ≤ ij.1 ∧ ij.1 < ij.2 ∧ ij.2 ≤ n ∧ + m = u ij.1 + u ij.2 + +/-- +`IsUlamSequence u` means that the sequence `u` satisfies the recurrence for Ulam's sequence: +`u 1 = 1`, `u 2 = 2`, and for `n ≥ 2`, `u (n+1)` is the least integer greater than `u n` +that has a unique representation as `u i + u j` with `1 ≤ i < j ≤ n`. +-/ +def IsUlamSequence (u : ℕ → ℕ) : Prop := + u 1 = 1 ∧ + u 2 = 2 ∧ + ∀ n : ℕ, 2 ≤ n → + u (n + 1) > u n ∧ + UniqueUlamSum u n (u (n + 1)) ∧ + ∀ m : ℕ, u n < m → UniqueUlamSum u n m → u (n + 1) ≤ m + +/-- +**Ulam pair conjecture** +There are infinitely many pairs of consecutive Ulam numbers differing by `2`. +-/ +@[category research open, AMS 11] +theorem ulam_infinitely_many_pairs : + answer(sorry) ↔ + ∀ u : ℕ → ℕ, IsUlamSequence u → + ∀ N : ℕ, ∃ n ≥ N, u (n + 1) = u n + 2 := by + sorry + +end Ulam From faa3a0528fe151138a1239fd90f34967cb5c8849 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Fri, 6 Mar 2026 10:31:38 -0800 Subject: [PATCH 02/10] Fix commenting --- FormalConjectures/ErdosProblems/342.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index 965ab4550..cd666af84 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -48,11 +48,10 @@ def IsUlamSequence (u : ℕ → ℕ) : Prop := ∀ m : ℕ, u n < m → UniqueUlamSum u n m → u (n + 1) ≤ m /-- -**Ulam pair conjecture** -There are infinitely many pairs of consecutive Ulam numbers differing by `2`. +Do infinitely many pairs (a, a+2) occur in Ulam's sequence? -/ -@[category research open, AMS 11] -theorem ulam_infinitely_many_pairs : +@[category research open, AMS 05 40] +theorem erdos_342_infinitely_many_pairs : answer(sorry) ↔ ∀ u : ℕ → ℕ, IsUlamSequence u → ∀ N : ℕ, ∃ n ≥ N, u (n + 1) = u n + 2 := by From eb86876220cc23b14e6ad93eee81ca44db09f558 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Sun, 8 Mar 2026 08:51:31 -0700 Subject: [PATCH 03/10] Apply suggestions from code review Co-authored-by: Moritz Firsching --- FormalConjectures/ErdosProblems/342.lean | 51 ++++++++++-------------- 1 file changed, 22 insertions(+), 29 deletions(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index cd666af84..731291f47 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -16,45 +16,38 @@ limitations under the License. import FormalConjectures.Util.ProblemImports /-! -# Erdos Problem 342 +# Erdős Problem 342 *References:* - [erdosproblems.com/342](https://www.erdosproblems.com/342) - [OEIS A002858](https://oeis.org/A002858) -/ -namespace Ulam +namespace Erdos342 -/-- -`UniqueUlamSum u n m` means that `m` has a unique representation as `u i + u j` -with `1 ≤ i < j ≤ n`. --/ -def UniqueUlamSum (u : ℕ → ℕ) (n m : ℕ) : Prop := - ∃! ij : ℕ × ℕ, - 1 ≤ ij.1 ∧ ij.1 < ij.2 ∧ ij.2 ≤ n ∧ - m = u ij.1 + u ij.2 +/-- `UniqueUlamSum a n m` means that $m$ has a unique representation as $a(i) + a(j)$ +with $i < j < n$. -/ +def UniqueUlamSum (a : ℕ → ℕ) (n m : ℕ) : Prop := + ∃! p : ℕ × ℕ, p.1 < p.2 ∧ p.2 < n ∧ m = a p.1 + a p.2 -/-- -`IsUlamSequence u` means that the sequence `u` satisfies the recurrence for Ulam's sequence: -`u 1 = 1`, `u 2 = 2`, and for `n ≥ 2`, `u (n+1)` is the least integer greater than `u n` -that has a unique representation as `u i + u j` with `1 ≤ i < j ≤ n`. --/ -def IsUlamSequence (u : ℕ → ℕ) : Prop := - u 1 = 1 ∧ - u 2 = 2 ∧ - ∀ n : ℕ, 2 ≤ n → - u (n + 1) > u n ∧ - UniqueUlamSum u n (u (n + 1)) ∧ - ∀ m : ℕ, u n < m → UniqueUlamSum u n m → u (n + 1) ≤ m +/-- `IsUlamSequence a` means that $a$ is the Ulam sequence (OEIS A002858): +$a(0) = 1$, $a(1) = 2$, and for each $n \geq 2$, $a(n)$ is the least integer +greater than $a(n-1)$ that has a unique representation as $a(i) + a(j)$ +with $i < j < n$. -/ +def IsUlamSequence (a : ℕ → ℕ) : Prop := + a 0 = 1 ∧ a 1 = 2 ∧ + ∀ n, 2 ≤ n → + a (n - 1) < a n ∧ + UniqueUlamSum a n (a n) ∧ + ∀ m, a (n - 1) < m → m < a n → ¬ UniqueUlamSum a n m /-- -Do infinitely many pairs (a, a+2) occur in Ulam's sequence? --/ -@[category research open, AMS 05 40] -theorem erdos_342_infinitely_many_pairs : +Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence? -/ +@[category research open, AMS 11] +theorem erdos_342.parts.i : answer(sorry) ↔ - ∀ u : ℕ → ℕ, IsUlamSequence u → - ∀ N : ℕ, ∃ n ≥ N, u (n + 1) = u n + 2 := by + ∀ a : ℕ → ℕ, IsUlamSequence a → + ∀ N : ℕ, ∃ n ≥ N, a (n + 1) = a n + 2 := by sorry -end Ulam +end Erdo342 From 3134b667dc6a809158fb6c175f401184de8d9814 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Sun, 8 Mar 2026 09:01:49 -0700 Subject: [PATCH 04/10] Fixes, add TODOs for other parts --- FormalConjectures/ErdosProblems/342.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index 731291f47..6eaed7b42 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -43,11 +43,15 @@ def IsUlamSequence (a : ℕ → ℕ) : Prop := /-- Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence? -/ -@[category research open, AMS 11] +@[category research open, AMS 05 11 40] theorem erdos_342.parts.i : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsUlamSequence a → ∀ N : ℕ, ∃ n ≥ N, a (n + 1) = a n + 2 := by sorry -end Erdo342 +-- TODO: Part (ii), does this sequence eventually have periodic differences? + +-- TODO: Part (iii), is the density of the sequence 0? Equivalently, Ben Green's problem 7: does this sequence have positive density? + +end Erdos342 From 13041a07b50bcf46b2d491a5e29a146f3dd846e7 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Sun, 8 Mar 2026 09:12:05 -0700 Subject: [PATCH 05/10] Formalize part (ii) similar to Erdos341, add Ben Green problem 7 to references --- FormalConjectures/ErdosProblems/342.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index 6eaed7b42..1b6c6a6bd 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -20,9 +20,13 @@ import FormalConjectures.Util.ProblemImports *References:* - [erdosproblems.com/342](https://www.erdosproblems.com/342) +- [Ben Green's Open Problem 7](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.7) - [OEIS A002858](https://oeis.org/A002858) -/ +open Nat Set Filter +open scoped Topology + namespace Erdos342 /-- `UniqueUlamSum a n m` means that $m$ has a unique representation as $a(i) + a(j)$ @@ -50,7 +54,16 @@ theorem erdos_342.parts.i : ∀ N : ℕ, ∃ n ≥ N, a (n + 1) = a n + 2 := by sorry --- TODO: Part (ii), does this sequence eventually have periodic differences? +/-- +Does Ulam's sequence eventually have periodic differences? That is, is $a(n+1) - a(n)$ eventually periodic? +-/ +@[category research open, AMS 05 11 40] +theorem erdos_342.parts.ii : + answer(sorry) ↔ + ∀ a : ℕ → ℕ, IsUlamSequence a → + let d : ℕ → ℤ := fun n ↦ (a (n + 1) : ℤ) - (a n : ℤ) + ∃ p > 0, ∀ᶠ m in atTop, d (m + p) = d m := by + sorry -- TODO: Part (iii), is the density of the sequence 0? Equivalently, Ben Green's problem 7: does this sequence have positive density? From a9be1e56cc5b3e9ed55188f3fd25398cd5861648 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Mon, 9 Mar 2026 10:19:25 -0700 Subject: [PATCH 06/10] Add third part --- FormalConjectures/ErdosProblems/342.lean | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index 1b6c6a6bd..ee75b22f1 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -51,7 +51,7 @@ Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence? -/ theorem erdos_342.parts.i : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsUlamSequence a → - ∀ N : ℕ, ∃ n ≥ N, a (n + 1) = a n + 2 := by + ∀ N : ℕ, ∃ n ≥ N, (a (n + 1)) = (a n) + 2 := by sorry /-- @@ -65,6 +65,17 @@ theorem erdos_342.parts.ii : ∃ p > 0, ∀ᶠ m in atTop, d (m + p) = d m := by sorry --- TODO: Part (iii), is the density of the sequence 0? Equivalently, Ben Green's problem 7: does this sequence have positive density? +/-- +Part (iii), is the density of the sequence 0? +-/ +@[category research open, AMS 05 11 40] +theorem erdos_342.parts.iii : + answer(sorry) ↔ + ∀ a : ℕ → ℕ, IsUlamSequence a → + Tendsto + (fun N : ℕ => + (Finset.card (Finset.filter (fun n ↦ a n ≤ N) (Finset.range N)) : ℝ) / N) + atTop (𝓝 0) := by + sorry end Erdos342 From 2bedbb4992c22bd49c47dd1351ccf378da075764 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Mon, 9 Mar 2026 17:17:59 -0700 Subject: [PATCH 07/10] add myself to authors :) --- AUTHORS | 1 + 1 file changed, 1 insertion(+) diff --git a/AUTHORS b/AUTHORS index 1c2da1d04..70908082c 100644 --- a/AUTHORS +++ b/AUTHORS @@ -8,6 +8,7 @@ Google LLC # Please keep the list sorted alphabetically Abel Doñate +Aditya Ramabadran Anirudh Rao Anthony Wang Ayush Debnath From d0128f12f803eb63aed73011c09fce0d4a9dcbc8 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Tue, 10 Mar 2026 07:21:10 -0700 Subject: [PATCH 08/10] Update FormalConjectures/ErdosProblems/342.lean Co-authored-by: Eric Wieser --- FormalConjectures/ErdosProblems/342.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index ee75b22f1..ae4514f8c 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -61,7 +61,7 @@ Does Ulam's sequence eventually have periodic differences? That is, is $a(n+1) - theorem erdos_342.parts.ii : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsUlamSequence a → - let d : ℕ → ℤ := fun n ↦ (a (n + 1) : ℤ) - (a n : ℤ) + let d (n : ℕ) : ℤ := a (n + 1) - a n ∃ p > 0, ∀ᶠ m in atTop, d (m + p) = d m := by sorry From c6d9a9f318bcdbd5804747cb1997ccaa2d6bdbc2 Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Mon, 16 Mar 2026 09:53:37 -0700 Subject: [PATCH 09/10] Apply suggestions from code review Co-authored-by: Moritz Firsching --- FormalConjectures/ErdosProblems/342.lean | 60 ++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index ae4514f8c..c137c55f6 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -22,6 +22,7 @@ import FormalConjectures.Util.ProblemImports - [erdosproblems.com/342](https://www.erdosproblems.com/342) - [Ben Green's Open Problem 7](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.7) - [OEIS A002858](https://oeis.org/A002858) +- [Gu04] Guy, Richard K., *Unsolved problems in number theory* (2004), xviii+437. -/ open Nat Set Filter @@ -45,6 +46,65 @@ def IsUlamSequence (a : ℕ → ℕ) : Prop := UniqueUlamSum a n (a n) ∧ ∀ m, a (n - 1) < m → m < a n → ¬ UniqueUlamSum a n m +/-- $a(0) = 1$ by definition. -/ +@[category test, AMS 5 11 40] +theorem erdos_342.test.a0 : ∀ a : ℕ → ℕ, IsUlamSequence a → a 0 = 1 := by + intro a ⟨ha0, _, _⟩; exact ha0 + +/-- $a(1) = 2$ by definition. -/ +@[category test, AMS 5 11 40] +theorem erdos_342.test.a1 : ∀ a : ℕ → ℕ, IsUlamSequence a → a 1 = 2 := by + intro a ⟨_, ha1, _⟩; exact ha1 + +/-- $a(2) = 3$: the only pair $(i,j)$ with $i < j < 2$ is $(0,1)$, giving $1 + 2 = 3$. -/ +@[category test, AMS 5 11 40] +theorem erdos_342.test.a2 : ∀ a : ℕ → ℕ, IsUlamSequence a → a 2 = 3 := by + intro a ⟨ha0, ha1, ha⟩ + obtain ⟨_, ⟨⟨i, j⟩, ⟨hij, hj, hsum⟩, _⟩, _⟩ := ha 2 (by omega) + interval_cases j <;> simp_all only [lt_one_iff, not_lt_zero'] + +/-- $a(3) = 4$: among sums $> 3$ with a unique representation from $\{1,2,3\}$, +the smallest is $4 = 1 + 3$. The candidate $5 = 2 + 3$ is ruled out by minimality since +$4$ has a unique representation. -/ +@[category test, AMS 05 11 40] +theorem erdos_342.test.a3 : ∀ a : ℕ → ℕ, IsUlamSequence a → a 3 = 4 := by + intro a ⟨ha0, ha1, ha⟩ + have ha2 := erdos_342.test.a2 a ⟨ha0, ha1, ha⟩ + obtain ⟨hinc, ⟨⟨i, j⟩, ⟨hij, hj, hsum⟩, _⟩, hmin⟩ := ha 3 (by omega) + simp only [show (3 : ℕ) - 1 = 2 from rfl] at hinc hmin + -- hinc : a 2 < a 3, hmin : ∀ m, a 2 < m → m < a 3 → ¬UniqueUlamSum a 3 m + -- hsum : a 3 = a i + a j, hij : i < j, hj : j < 3 + -- Enumerate j ∈ {0, 1, 2} + interval_cases j + · -- j = 0: i < 0 impossible + omega + · -- j = 1: i = 0, so a 3 = a 0 + a 1 = 1 + 2 = 3, but a 3 > a 2 = 3 + have hi : i = 0 := by omega + subst hi; rw [ha0, ha1] at hsum; rw [ha2] at hinc; omega + · -- j = 2 + interval_cases i + · -- i = 0: a 3 = a 0 + a 2 = 1 + 3 = 4 + rw [ha0, ha2] at hsum; exact hsum + · -- i = 1: a 3 = a 1 + a 2 = 2 + 3 = 5 + rw [ha1, ha2] at hsum + -- hsum : a 3 = 5. Use minimality: m = 4 has unique sum, contradiction. + exfalso + have h4 := hmin 4 (by rw [ha2]; omega) (by omega) + apply h4 + -- Goal: UniqueUlamSum a 3 4, i.e. ∃! (p : ℕ × ℕ), p.1 < p.2 ∧ p.2 < 3 ∧ 4 = a p.1 + a p.2 + -- Witness: (0, 2) since a 0 + a 2 = 1 + 3 = 4 + refine ⟨⟨0, 2⟩, ⟨by omega, by omega, by rw [ha0, ha2]⟩, ?_⟩ + -- Uniqueness: check all pairs (i', j') with i' < j' < 3 + rintro ⟨i', j'⟩ ⟨hij', hj', hsum'⟩ + simp only [Prod.mk.injEq] + interval_cases j' + · omega + · interval_cases i' + · rw [ha0, ha1] at hsum'; omega + · interval_cases i' + · rw [ha0, ha2] at hsum'; constructor <;> omega + · rw [ha1, ha2] at hsum'; omega + /-- Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence? -/ @[category research open, AMS 05 11 40] From 6e29790bcc0d652fcbb70b409505050da0aa325a Mon Sep 17 00:00:00 2001 From: Aditya Ramabadran Date: Tue, 17 Mar 2026 09:03:23 -0700 Subject: [PATCH 10/10] Apply suggestions from code review Co-authored-by: Moritz Firsching --- FormalConjectures/ErdosProblems/342.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/FormalConjectures/ErdosProblems/342.lean b/FormalConjectures/ErdosProblems/342.lean index c137c55f6..fd32c41ac 100644 --- a/FormalConjectures/ErdosProblems/342.lean +++ b/FormalConjectures/ErdosProblems/342.lean @@ -111,7 +111,7 @@ Do infinitely many pairs $(a, a+2)$ occur in Ulam's sequence? -/ theorem erdos_342.parts.i : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsUlamSequence a → - ∀ N : ℕ, ∃ n ≥ N, (a (n + 1)) = (a n) + 2 := by + Set.Infinite {n : ℕ | ∃ m, a m = a n + 2} := by sorry /-- @@ -132,10 +132,7 @@ Part (iii), is the density of the sequence 0? theorem erdos_342.parts.iii : answer(sorry) ↔ ∀ a : ℕ → ℕ, IsUlamSequence a → - Tendsto - (fun N : ℕ => - (Finset.card (Finset.filter (fun n ↦ a n ≤ N) (Finset.range N)) : ℝ) / N) - atTop (𝓝 0) := by + Set.upperDensity (Set.range a) = 0 := by sorry end Erdos342