Erdős problem 456

Erdős [Er79e] writes it is 'easy to show' that for infinitely many $n$ we have $m_n < p_n$ .

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

456.lean

Retained formal statement6 of 7

Erdős [Er79e] writes it is 'easy to show' that $m_n/n \to \infty$ for almost all $n$ .

FormalConjectures/ErdosProblems/456.leanErdos456.erdos_456.variants.m_div_n3 linesExact file

1∃ A,2  Filter.Tendsto (fun N => ↑(Nat.count A N) / ↑N) Filter.atTop (nhds 1) ∧3    Filter.Tendsto (fun n => ↑(Erdos456.m n) / ↑n) (Filter.atTop ⊓ Filter.principal A) Filter.atTop

SolvedStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures7
statement retained
VibeMathed0
not observed here
PLBY Lean proofs0
not observed here
Jayyhk Erdős Lean0
not observed here
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki1
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 456.lean7