feat(ErdosProblems): 375 #1497

CoolRmal · 2026-01-05T23:09:01Z

Closes #699

I only include the strongest result.

FormalConjectures/ErdosProblems/375.lean

Co-authored-by: Yaël Dillies <[email protected]>

FormalConjectures/Wikipedia/LegendreConjecture.lean

CoolRmal · 2026-01-07T07:52:35Z

I think I addressed all your comments. I'll work on the proof of bounded_gap_legendre.

YaelDillies · 2026-01-07T08:34:14Z

Do you want to prove it in this PR or the next one?

…ures into Erdos375

CoolRmal · 2026-01-08T00:15:10Z

FormalConjectures/Wikipedia/LegendreConjecture.lean

+    (∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <
+    (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c))
+    → ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p := by


After some thoughts, I think they only want the statement to be true eventually, because otherwise we are assuming the following two (and potentially more) absurd inequalities:

$2 = 5 - 3 < 3 ^ {1 / 2 - c}$

$4 = 11 - 7 < 7 ^ {1/2 - c }$

I also used Nat.Prime instead of Prime.

But then the Ferreira statement below is the same but unconditional, right? @mo271, what do you suggest here?

I agree with @YaelDillies on this one: I think the goal of the theorem should quantify over all n (but this is fine: to avoid the absurd inequalities you mention we only need to take sufficiently large n in the hypothesis of the theorem)

@Paul-Lez Should I keep this theorem then? I think Yaël is suggesting that this theorem is not needed because it is not better than Ferreira's statement.

I think I have convinced myself that this statement is worth having on the basis that what we're interested in in this repo isn't results but proofs. An AI proving the implication you are adding would be interested, even if the statement can theoretically be made stronger

Paul-Lez

Thanks for the PR! Added a few comments

Paul-Lez · 2026-01-16T10:24:52Z

FormalConjectures/ErdosProblems/375.lean

+/-- Is it true that for any `n ≥ 1` and any `k`, if `n + 1, ..., n + k` are all composite, then
+there are distinct primes `p₁, ... pₖ` such that `pᵢ ∣ n + i` for all `1 ≤ i ≤ k`? -/
+@[category research open, AMS 11]
+theorem erdos_375 : answer(sorry) ↔ ∀ n ≥ 1, ∀ k, (∀ i < k, ¬ (n + i + 1).Prime) →


Given that you're using erdos_375 as as assumption later on, I would suggest the following:

Define a predicate Erdos375 (as a def)

State erdos_375 as answer(sorry) ↔ erdos_375

State the other implications using Erdos375.

This will help with maintainability (e.g. only need to fix the statement of erdos_375 once if it breaks) and readability of the downstream implications!

Paul-Lez · 2026-01-16T10:28:02Z

FormalConjectures/ErdosProblems/375.lean

+    · exact this n hn k hk h p hp y x hxy.symm hr.symm (by grind)
+    · have hy : y = x + 1 := by grind
+      have := hy ▸ Nat.dvd_sub (hp y).2 (hxy ▸ (hp x).2)
+      have := (hp 1).1


(very nitpicky) you can get rid of this line

Suggested change

have := (hp 1).1

The goal is not solved if I delete this line.

Paul-Lez · 2026-01-16T10:29:38Z

FormalConjectures/ErdosProblems/375.lean

+there are distinct primes `p₁, ... pₖ` such that `pᵢ ∣ n + i` for all `1 ≤ i ≤ k`. This is proved
+in [RST75]. -/
+@[category research solved, AMS 11]
+theorem erdos_375.log : ∃ c > 0, ∀ n k : ℕ,


I think the "n sufficiently large" condition is missing otherwise?

Suggested change

theorem erdos_375.log : ∃ c > 0, ∀ n k : ℕ,

theorem erdos_375.log : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ k : ℕ,

Yael suggested me this. The reason is that one can always take c small enough so that k < c * (log n / (log (log n))) implies that k : ℕ is zero until n is large.

Paul-Lez · 2026-01-16T10:36:27Z

FormalConjectures/Wikipedia/LegendreConjecture.lean

+    (∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <
+    (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c))
+    → ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p := by


I agree with @YaelDillies on this one: I think the goal of the theorem should quantify over all n (but this is fine: to avoid the absurd inequalities you mention we only need to take sufficiently large n in the hypothesis of the theorem)

Paul-Lez · 2026-01-16T10:37:25Z

FormalConjectures/Wikipedia/LegendreConjecture.lean

+/-- If there exists a constant `c > 0` such that
+`(n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c)` for all `n`, then
+Legendre's conjecture is true. -/
+@[category research solved, AMS 11]
+theorem bounded_gap_legendre :
+    (∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <
+    (n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c))
+    → ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p := by


Suggested change

/-- If there exists a constant `c > 0` such that

`(n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c)` for all `n`, then

Legendre's conjecture is true. -/

@[category research solved, AMS 11]

theorem bounded_gap_legendre :

(∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <

(n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c))

→ ∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p := by

/-- If there exists a constant `c > 0` such that

`(n + 1).nth Nat.Prime - n.nth Nat.Prime < (n.nth Nat.Prime) ^ (1 / 2 - c)` for sufficiently large `n`, then

Legendre's conjecture is true. -/

@[category research solved, AMS 11]

theorem bounded_gap_legendre

(H : ∃ c > 0, ∀ᶠ n in atTop, (n + 1).nth Nat.Prime - n.nth Nat.Prime <

(n.nth Nat.Prime : ℝ) ^ (1 / (2 : ℝ) - c)) :

∀ᶠ n in atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Prime p := by

FormalConjectures/Wikipedia/LegendreConjecture.lean

Co-authored-by: Yaël Dillies <[email protected]>

CoolRmal added 2 commits January 5, 2026 15:36

Create 375.lean

452796f

Update 375.lean

7974a61

YaelDillies reviewed Jan 6, 2026

View reviewed changes

YaelDillies added ams-11: Number theory erdos-problems Erdős Problems awaiting-author The author should answer a question or perform changes. Reply when done. labels Jan 6, 2026

CoolRmal and others added 4 commits January 6, 2026 13:00

Update FormalConjectures/ErdosProblems/375.lean

c377244

Co-authored-by: Yaël Dillies <[email protected]>

Update 375.lean

3c450a7

Update 375.lean

f335d7e

gap

2771ad2

github-actions bot added the wikipedia label Jan 6, 2026

CoolRmal added 2 commits January 7, 2026 00:38

Merge branch 'main' into Erdos375

4b55823

legendre

888f92b

YaelDillies reviewed Jan 7, 2026

View reviewed changes

Update LegendreConjecture.lean

66da6e1

YaelDillies reviewed Jan 7, 2026

View reviewed changes

FormalConjectures/Wikipedia/LegendreConjecture.lean Outdated Show resolved Hide resolved

Update LegendreConjecture.lean

5dfb879

YaelDillies removed the awaiting-author The author should answer a question or perform changes. Reply when done. label Jan 7, 2026

YaelDillies and others added 3 commits January 7, 2026 09:34

nit

29ef4fc

Merge branch 'Erdos375' of https://github.com/CoolRmal/formal-conject…

993372e

…ures into Erdos375

docstring

fb7a9ed

CoolRmal commented Jan 8, 2026

View reviewed changes

Update 375.lean

eaa6945

Paul-Lez reviewed Jan 16, 2026

View reviewed changes

update

9ddac1f

YaelDillies reviewed Jan 17, 2026

View reviewed changes

FormalConjectures/Wikipedia/LegendreConjecture.lean Outdated Show resolved Hide resolved

Update FormalConjectures/Wikipedia/LegendreConjecture.lean

0642840

Co-authored-by: Yaël Dillies <[email protected]>

	theorem erdos_375.log : ∃ c > 0, ∀ n k : ℕ,
	theorem erdos_375.log : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ k : ℕ,

feat(ErdosProblems): 375 #1497

Are you sure you want to change the base?

feat(ErdosProblems): 375 #1497

Conversation

CoolRmal commented Jan 5, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

CoolRmal commented Jan 7, 2026

Uh oh!

YaelDillies commented Jan 7, 2026

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!

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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants