feat(ErdosProblems): formalize 423, 839 by ryantuck · Pull Request #3586 · google-deepmind/formal-conjectures

ryantuck · 2026-03-17T15:12:33Z

Followup to #3422, which formalized all remaining conjectures, but breaking out into a few manageable-sized PRs, split by category. See that original PR for the specific rigor applied to the AI pipeline to ensure these formalizations were produced up to a reasonable standard.

This PR contains three open Erdos problems that Claude categorized as sequences_asymptotics.

fixes #722
fixes #971

mo271 · 2026-03-17T15:23:20Z

Thanks!
Note that for 342 is already almost ready to merged:
#3438

I picked one thing that was more idiomatic here and added it to the review there, so thanks for that!
Makes sense to compare them more closely to take the best of boths, but I think it is best to drop this problem from the pull request here.

mo271 · 2026-03-17T15:25:16Z

+      ∃ N p : ℕ, 0 < p ∧ ∀ n, N ≤ n →
+        a (n + p + 1) - a (n + p) = a (n + 1) - a n := by


this is better done using ∀ᶠ m in atTop as in #3438

mo271 · 2026-03-17T15:28:16Z

when adding "fixes #[issue number]" in the pull request description it automatically links them to avoid duplicate work on it and the issues will get closed automatically when merged

ryantuck · 2026-03-17T15:53:41Z

@mo271 I've removed 342 from this PR, and have included the "fixes: NUM" syntax in subsequent related PRs.

mo271

Many Thanks -- plenty good things in here. Most noticeable all math correct, often also idiomatic. Just some suggestions mainly on style.
One major missing point: Problem 423 is missing main problem.

mo271 · 2026-03-17T15:58:06Z

+-/
+
+import FormalConjectures.Util.ProblemImports
+import FormalConjecturesForMathlib.Data.Set.Density


Suggested change

import FormalConjecturesForMathlib.Data.Set.Density

Those imports are automatic when inlcuding the ProblemImports

mo271 · 2026-03-17T16:08:46Z

+Let $a_1 = 1$ and $a_2 = 2$, and for $k \ge 3$ choose $a_k$ to be the least integer
+$> a_{k-1}$ which is the sum of at least two consecutive terms of the sequence. What is
+the asymptotic behaviour of this sequence?
+
+The sequence begins $1, 2, 3, 5, 6, 8, 10, 11, \ldots$ (OEIS A005243).
+
+Asked by Hofstadter (Erdős says Hofstadter was inspired by a similar question of Ulam).
+Bolan and Tang have independently proved that $a_n - n$ is nondecreasing and unbounded,
+so there are infinitely many integers not appearing in the sequence.


Let's not repeat the problem here, those comments should go the definition of the sequence the corresponding conjectures/theorems.

mo271 · 2026-03-17T16:10:48Z

+*Reference:* [erdosproblems.com/423](https://www.erdosproblems.com/423)
+
+Let $a_1 = 1$ and $a_2 = 2$, and for $k \ge 3$ choose $a_k$ to be the least integer
+$> a_{k-1}$ which is the sum of at least two consecutive terms of the sequence. What is
+the asymptotic behaviour of this sequence?
+
+The sequence begins $1, 2, 3, 5, 6, 8, 10, 11, \ldots$ (OEIS A005243).
+
+Asked by Hofstadter (Erdős says Hofstadter was inspired by a similar question of Ulam).
+Bolan and Tang have independently proved that $a_n - n$ is nondecreasing and unbounded,
+so there are infinitely many integers not appearing in the sequence.
+
+[Er77c] Erdős, P., *Problems and results on combinatorial number theory. III*,
+Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72.
+
+[ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial
+number theory*, Monographies de L'Enseignement Mathématique (1980).
+
+[Bolan] Bolan, M., *Hofstader–Ulam Sequence*,
+https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf
+
+[Tang] Tang, Q., *On Erdős Problem 423*,
+https://github.com/QuanyuTang/erdos-problem-423/blob/main/On_Erd%C5%91s_Problem_423.pdf


Suggested change

*Reference:* [erdosproblems.com/423](https://www.erdosproblems.com/423)

Let $a_1 = 1$ and $a_2 = 2$, and for $k \ge 3$ choose $a_k$ to be the least integer

$> a_{k-1}$ which is the sum of at least two consecutive terms of the sequence. What is

the asymptotic behaviour of this sequence?

The sequence begins $1, 2, 3, 5, 6, 8, 10, 11, \ldots$ (OEIS A005243).

Asked by Hofstadter (Erdős says Hofstadter was inspired by a similar question of Ulam).

Bolan and Tang have independently proved that $a_n - n$ is nondecreasing and unbounded,

so there are infinitely many integers not appearing in the sequence.

[Er77c] Erdős, P., *Problems and results on combinatorial number theory. III*,

Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72.

[ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial

number theory*, Monographies de L'Enseignement Mathématique (1980).

[Bolan] Bolan, M., *Hofstader–Ulam Sequence*,

https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf

[Tang] Tang, Q., *On Erdős Problem 423*,

https://github.com/QuanyuTang/erdos-problem-423/blob/main/On_Erd%C5%91s_Problem_423.pdf

*References:*

- [erdosproblems.com/423](https://www.erdosproblems.com/423)

- [Er77c] Erdős, P., *Problems and results on combinatorial number theory. III*,

Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976), 1977, pp. 43–72.

- [ErGr80] Erdős, P. and Graham, R., *Old and new problems and results in combinatorial

number theory*, Monographies de L'Enseignement Mathématique (1980).

- [Bolan] Bolan, M., *Hofstader–Ulam Sequence*,

https://github.com/mjtb49/HofstaderUlam/blob/main/HofstaderUlamSequence.pdf

- [Tang] Tang, Q., *On Erdős Problem 423*,

https://github.com/QuanyuTang/erdos-problem-423/blob/main/On_Erd%C5%91s_Problem_423.pdf

- [OEIS A5243](https://oeis.org/A5243)

not the added OEIS reference (it was mentioned before, now listed in the reference with link)

mo271 · 2026-03-17T16:20:00Z

+Tang.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_423_nondecreasing :


Suggested change

theorem erdos_423_nondecreasing :

theorem erdos_423.variants.nondecreasing :

there is a README.md in FormalConjectures/ErdosProblems/ explaining the naming convention.

mo271 · 2026-03-17T16:22:18Z

+of the sequence remains an open question.
+-/
+@[category research solved, AMS 5 11]
+theorem erdos_423 :


Suggested change

theorem erdos_423 :

theorem erdos_423.variants.unbounded :

this is not the main variant here!

mo271 · 2026-03-17T19:15:08Z

+@[category research open, AMS 11]
+theorem erdos_839 : answer(sorry) ↔
+    ∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
+    ∀ M : ℝ, ∃ᶠ n in atTop, M < (a n : ℝ) / (n : ℝ) := by


Better to use limsup, because closer to informal formulation

Suggested change

∀ M : ℝ, ∃ᶠ n in atTop, M < (a n : ℝ) / (n : ℝ) := by

atTop.limsup (fun n : ℕ => (a n : ℝ≥0∞) / n) = ⊤ := by

with open scoped ENNReal

Or limsup (fun n : ℕ => (a n : ℝ≥0∞) / n) atTop = ⊤

mo271 · 2026-03-17T19:20:14Z

+
+Let $1 \leq a_1 < a_2 < \cdots$ be a strictly increasing sequence of positive integers
+such that no $a_i$ is the sum of consecutive $a_j$ for $j < i$.
+Is it true that $\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0$?


Suggested change

Is it true that $\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0$?

Is it true that $\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0$?

This is equivalent to asking whether the range $\{a_1, a_2, \ldots\}$ has logarithmic density

zero (see `Set.HasLogDensity`).

Good usage of this, instead of the manual definition!

mo271 · 2026-03-17T19:23:32Z

+    ∀ (a : ℕ → ℕ), (∀ n, 1 ≤ a n) → StrictMono a → SumOfConsecutiveFree a →
+    Set.HasLogDensity (Set.range a) 0 := by
+  sorry
+


Please add a --TODO for the additional material
(This tries to preserve the invariant: if a file is present and there are no TODOs, then it reflects what was on erdosproblems.com at the time of writing...)

mo271 · 2026-03-17T19:25:06Z

+Is it true that $\limsup a_n / n = \infty$?
+-/
+@[category research open, AMS 11]
+theorem erdos_839 : answer(sorry) ↔


Suggested change

theorem erdos_839 : answer(sorry) ↔

theorem erdos_839.parts.i : answer(sorry) ↔

is the naming convention, I think

mo271 · 2026-03-17T19:25:43Z

+Is it true that $\lim_{x \to \infty} \frac{1}{\log x} \sum_{a_n < x} \frac{1}{a_n} = 0$?
+-/
+@[category research open, AMS 11]
+theorem erdos_839.variants.stronger : answer(sorry) ↔


Suggested change

theorem erdos_839.variants.stronger : answer(sorry) ↔

theorem erdos_839.parts.ii : answer(sorry) ↔

this is not from the additional material, hence a parts not a variant.

feat(ErdosProblems): formalize 342, 423, 839

ac19447

github-actions bot added the erdos-problems Erdős Problems label Mar 17, 2026

mo271 mentioned this pull request Mar 17, 2026

feat(ErdosProblems/342) #3438

Merged

mo271 reviewed Mar 17, 2026

View reviewed changes

ryantuck mentioned this pull request Mar 17, 2026

feat(ErdosProblems): All 1179 Erdős conjectures formalized #3422

Open

rm 342 (in progress elsewhere)

0b6b154

ryantuck changed the title ~~feat(ErdosProblems): formalize 342, 423, 839~~ feat(ErdosProblems): formalize 423, 839 Mar 17, 2026

mo271 reviewed Mar 17, 2026

View reviewed changes

mo271 added the awaiting-author The author should answer a question or perform changes. Reply when done. label Mar 22, 2026

		∃ N p : ℕ, 0 < p ∧ ∀ n, N ≤ n →
		a (n + p + 1) - a (n + p) = a (n + 1) - a n := by

	theorem erdos_423_nondecreasing :
	theorem erdos_423.variants.nondecreasing :

	∀ M : ℝ, ∃ᶠ n in atTop, M < (a n : ℝ) / (n : ℝ) := by
	atTop.limsup (fun n : ℕ => (a n : ℝ≥0∞) / n) = ⊤ := by

	theorem erdos_839 : answer(sorry) ↔
	theorem erdos_839.parts.i : answer(sorry) ↔

	theorem erdos_839.variants.stronger : answer(sorry) ↔
	theorem erdos_839.parts.ii : answer(sorry) ↔

Conversation

ryantuck commented Mar 17, 2026 • edited by mo271 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mo271 commented Mar 17, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mo271 commented Mar 17, 2026

Uh oh!

ryantuck commented Mar 17, 2026

Uh oh!

mo271 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ryantuck commented Mar 17, 2026 •

edited by mo271

Loading