Erdős problem 375 · problems.science

Is Erdos375Prop true?

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

375.lean

Retained formal statement4 of 5

In particular, if Erdos375Prop is true, then Legendre's conjecture is asymptotically true.

FormalConjectures/ErdosProblems/375.leanErdos375.erdos_375.variants.legendre1 lineExact file

1Erdos375.Erdos375Prop → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

SolvedStatement only, no proof