feat(ErdosProblems): 884 #1248

kesslermaximilian · 2025-11-20T23:46:56Z

Formalizes https://www.erdosproblems.com/884.
Closes #1001.

A few questions: I wasn't able to find mathlib functionality for the ordered list of divisors of a natural number, so I quickly wrote my own abbreviation.

Also, would it fit the project scope to also formalize the statement of Tao's paper, disproving this conjecture under assumption of hardy-littlewood? If so, there is currently only the general hardy-littlewood statement formalized in this repository, but Tao only requires a qualitative statement about existence, not density of admissable prime-tuples.

Formalizes https://www.erdosproblems.com/884. Closes google-deepmind#1001.

google-cla · 2025-11-20T23:47:01Z

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

kesslermaximilian · 2025-11-20T23:54:40Z

Edit: I fixed the issue myself.

I'm trying to sign the CLA right now, which I did with some google-account now (meh...). However, in the troubleshooting explanation, I am confused by the line:

You may not be using the email associated with your CLA in your Git commits. Check that the email set on your git commits matches the email associated with your CLA.
Does that mean that I have to make my git commits using a gmail-address? Do I need to somehow link the gmail with my github?
I'd appreciate some help in how I can resolve this, thanks in advance.

mo271 · 2025-11-21T08:43:54Z

Seems like it works now? Do you still need help here?
you can change the author of a commit later

 git commit --amend --author="Your Name <your_name@gmail.com>" --no-edit

and then force push.
To see what email address was used you can do git log or add patch to the github url for the commit:
https://github.com/google-deepmind/formal-conjectures/commit/30528027c6f71f889497b1f889607244284c48ed.patch

I think if you add multiple email addresses to your github account you can sign the CLA only with one of them and it should still work for the other ones?

kesslermaximilian · 2025-11-21T16:46:18Z

Yeah, regarding the CLA, things worked out now. But obviously, this PR still needs to be reviewed, etc.

callesonne · 2025-11-23T22:33:08Z

FormalConjectures/ErdosProblems/884.lean

+By convention, we set `divisors_increasing 0 = ∅`.
+As a `Finset`, this is the same as `Nat.divisors`
+-/
+abbrev divisors_increasing (n : ℕ) : List ℕ := (List.range (n + 1)).filter (· ∣ n)


Instead of defining this, I would use Nat.nth (· ∣ n) i to pick out the i:th smallest divisor of n (to answer the question in the PR description).

I agree with Calle on this one. Note that you could also define this as n.divisors.sort.

Thanks for the suggestion, I updated my code accordingly.

Thanks! Make sure to also delete the old divisors_increasing

Paul-Lez · 2025-11-27T10:37:54Z

FormalConjectures/ErdosProblems/884.lean

+By convention, we set `divisors_increasing 0 = ∅`.
+As a `Finset`, this is the same as `Nat.divisors`
+-/
+abbrev divisors_increasing (n : ℕ) : List ℕ := (List.range (n + 1)).filter (· ∣ n)


I agree with Calle on this one. Note that you could also define this as n.divisors.sort.

FormalConjectures/ErdosProblems/884.lean

…ctures into erdos-884

kesslermaximilian · 2025-11-27T14:10:34Z

Thanks for your comments / review. I updated the PR using your suggestions now.

smmercuri · 2025-11-28T11:35:12Z

FormalConjectures/ErdosProblems/884.lean

+Statement of Erdos conjecture 884. See `erdos_884` for the problem asking whether this is true.
+-/
+def erdos_884_stmt : Prop :=
+    sum_inv_of_divisor_pair_differences =O[Filter.atTop] (1 + sum_inv_of_divisor_pair_differences)


Shouldn't the RHS be 1 + sum_inv_of_consecutive_divisors?

Oh yes, of course.
Thanks for catching that

I pushed a new commit fixing this

callesonne

Some more comments :)

callesonne · 2025-12-04T14:39:13Z

FormalConjectures/ErdosProblems/884.lean

+For a natural number n, let `1 = d₁ < ⋯ < d_{τ(n)} = n` denote the divisors of n
+in increasing order.
+Does it hold that
+`∑ 1 ≤ i < j ≤ τ(n), 1 / (d_j - d_i) ⟪ 1 + ∑ 1 ≤ i < τ(n), 1 / (d_{i + 1} - d_i)`
+for `n → ∞`, i.e.
+`∑ 1 ≤ i < j ≤ τ(n), 1 / (d_j - d_i) ∈ O (1 + ∑ 1 ≤ i < τ(n), 1 / (d_{i + 1} - d_i))`?
+
+In September 2025, Terence Tao gave a conditional _negative_ answer to this conjecture,
+see `erdos_884_fales_of_hardy_littlewood` for this implication.
+However, the conjecture itself remains open.


We usually write our docstrings over erdos problems using latex. Could you also do this?

yes, I did so now

callesonne · 2025-12-04T14:39:40Z

FormalConjectures/ErdosProblems/884.lean

+/--
+Statement of Erdos conjecture 884. See `erdos_884` for the problem asking whether this is true.
+-/


Could you include the problem statement in this docstring as well (you can copy-paste from below if you wish).

callesonne · 2025-12-04T14:44:34Z

FormalConjectures/ErdosProblems/884.lean

+Statement of Erdos conjecture 884. See `erdos_884` for the problem asking whether this is true.
+-/
+def erdos_884_stmt : Prop :=
+    sum_inv_of_divisor_pair_differences =O[Filter.atTop] (1 + sum_inv_of_consecutive_divisors)


Suggested change

sum_inv_of_divisor_pair_differences =O[Filter.atTop] (1 + sum_inv_of_consecutive_divisors)

sum_inv_of_divisor_pair_differences ≪ 1 + sum_inv_of_consecutive_divisors

We have this notation in ForMathlib (and I think you should be able to remove the parenthesis).

thanks, I did not know this notation, I inserted it now

callesonne · 2025-12-04T14:48:03Z

FormalConjectures/ErdosProblems/884.lean

+By convention, we set `divisors_increasing 0 = ∅`.
+As a `Finset`, this is the same as `Nat.divisors`
+-/
+abbrev divisors_increasing (n : ℕ) : List ℕ := (List.range (n + 1)).filter (· ∣ n)


Please remove this now that it is not used anymore.

oh yes, done

- Write doc comment in LaTeX. - Remove divisors_increasing definition - Use notation for BigO - Copy doc comment to problem statement as well

kesslermaximilian · 2026-01-19T16:32:51Z

Hey. Sorry for the long period of inactivity. I responded to all the comments from the review now and updated the PR.
Thanks for your patience and the (continued) feedback

Paul-Lez

A few minor nitpicks and then this should be ready to merge!

Paul-Lez · 2026-01-19T16:49:09Z

FormalConjectures/ErdosProblems/884.lean

+@[category research solved, AMS 11]
+theorem erdos_884_false_of_hardy_littlewood :
+    ∀ (k : ℕ) (m : Fin k.succ → ℕ), HardyLittlewood.FirstHardyLittlewoodConjectureFor m
+    → ¬ erdos_884_stmt := by sorry


Suggested change

→ ¬ erdos_884_stmt := by sorry

→ ¬ erdos_884_stmt := by

sorry

Paul-Lez · 2026-01-19T16:49:36Z

FormalConjectures/ErdosProblems/884.lean

+see `erdos_884_false_of_hardy_littlewood` for this implication.
+However, the conjecture itself remains open.
+-/
+def erdos_884_stmt : Prop :=


(to stick a little closer to this repo's convention!)

Suggested change

def erdos_884_stmt : Prop :=

def Erdos884 : Prop :=

Paul-Lez · 2026-01-19T16:52:07Z

FormalConjectures/ErdosProblems/884.lean

+
+namespace Erdos884
+
+noncomputable abbrev sum_inv_of_divisor_pair_differences (n : ℕ) : ℚ :=


I'd suggest this name to sick a little closer to the Mathlib naming conventions

Suggested change

noncomputable abbrev sum_inv_of_divisor_pair_differences (n : ℕ) : ℚ :=

noncomputable abbrev sumDivisorInvPairwiseDifference (n : ℕ) : ℚ :=

Paul-Lez · 2026-01-19T16:52:48Z

FormalConjectures/ErdosProblems/884.lean

+    ∑ j : Fin n.divisors.card, ∑ i : Fin  j,
+    (1 : ℚ) / (Nat.nth (· ∣ n) j - Nat.nth (· ∣ n) i )
+
+noncomputable abbrev sum_inv_of_consecutive_divisors (n : ℕ) : ℚ :=


Suggested change

noncomputable abbrev sum_inv_of_consecutive_divisors (n : ℕ) : ℚ :=

noncomputable abbrev sumDivisorInvConsecutiveDifference (n : ℕ) : ℚ :=

kesslermaximilian · 2026-01-20T14:25:53Z

Thanks, updated the PR according to your feedback.

kesslermaximilian · 2026-01-25T23:23:39Z

@Paul-Lez Not trying to rush you, just wanted to check in whether you saw that I updated the PR. I appreciate all your time and effort you put into this as well.

Add Erdos Problem 884

3052802

Formalizes https://www.erdosproblems.com/884. Closes google-deepmind#1001.

mo271 added the erdos-problems Erdős Problems label Nov 21, 2025

Merge branch 'main' into erdos-884

8525c36

callesonne reviewed Nov 23, 2025

View reviewed changes

Paul-Lez reviewed Nov 27, 2025

View reviewed changes

kesslermaximilian and others added 4 commits November 27, 2025 14:30

use Nat.nth (· ∣ n) to pick out divisors of n

cc4212f

add implication of hardy-littlewood => erdos 884 false

439971c

Merge branch 'erdos-884' of github.com:kesslermaximilian/formal-conje…

c5defc2

…ctures into erdos-884

Merge branch 'main' into erdos-884

2069319

smmercuri reviewed Nov 28, 2025

View reviewed changes

fix: use correct sum on RHS

530aa3d

callesonne reviewed Dec 4, 2025

View reviewed changes

YaelDillies added the awaiting-author The author should answer a question or perform changes. Reply when done. label Dec 9, 2025

YaelDillies changed the title ~~Add Erdos Problem 884~~ feat(ErdosProblems): 884 Jan 3, 2026

Respond to PR review

3a6abde

- Write doc comment in LaTeX. - Remove divisors_increasing definition - Use notation for BigO - Copy doc comment to problem statement as well

kesslermaximilian force-pushed the erdos-884 branch from a3e08f4 to 3a6abde Compare January 19, 2026 16:31

Paul-Lez reviewed Jan 19, 2026

View reviewed changes

respond to code review

d3087b9

	sum_inv_of_divisor_pair_differences =O[Filter.atTop] (1 + sum_inv_of_consecutive_divisors)
	sum_inv_of_divisor_pair_differences ≪ 1 + sum_inv_of_consecutive_divisors

	→ ¬ erdos_884_stmt := by sorry
	→ ¬ erdos_884_stmt := by
	sorry


		namespace Erdos884

		noncomputable abbrev sum_inv_of_divisor_pair_differences (n : ℕ) : ℚ :=

	noncomputable abbrev sum_inv_of_divisor_pair_differences (n : ℕ) : ℚ :=
	noncomputable abbrev sumDivisorInvPairwiseDifference (n : ℕ) : ℚ :=

	noncomputable abbrev sum_inv_of_consecutive_divisors (n : ℕ) : ℚ :=
	noncomputable abbrev sumDivisorInvConsecutiveDifference (n : ℕ) : ℚ :=

feat(ErdosProblems): 884 #1248

Are you sure you want to change the base?

feat(ErdosProblems): 884 #1248

Uh oh!

Conversation

kesslermaximilian commented Nov 20, 2025

Uh oh!

google-cla bot commented Nov 20, 2025

Uh oh!

kesslermaximilian commented Nov 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mo271 commented Nov 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kesslermaximilian commented Nov 21, 2025

Uh oh!

callesonne Nov 23, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

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!

Uh oh!

kesslermaximilian commented Nov 27, 2025

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!

callesonne 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!

kesslermaximilian commented Jan 19, 2026

Uh oh!

Paul-Lez 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!

kesslermaximilian commented Jan 20, 2026

Uh oh!

kesslermaximilian commented Jan 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

kesslermaximilian commented Nov 20, 2025 •

edited

Loading

mo271 commented Nov 21, 2025 •

edited

Loading

callesonne Nov 23, 2025 •

edited

Loading