Skip to content

Erdős problem 770

Start work

For odd n, the values of h n form an unbounded set. This is described as 'easy to see' in [Er74b].

Sources

The source's own material, retained exactly.

6 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

770.lean

Retained formal statement3 of 6

Is it true that if p is the greatest prime such that p - 1 ∣ n and p > n ^ ε, then h n = p?

FormalConjectures/ErdosProblems/770.leanErdos770.erdos_770.parts.iii5 linesExact file
sorry ↔  ∀ ε > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      have p := sSup {m | Nat.Prime m ∧ m - 1 ∣ n};      ↑p > ↑n ^ ε → Erdos770.h n = ↑p
OpenStatement only, no proof