Skip to content

Erdős problem 82

Start work

F(n)/log⁡n→∞asn→∞F(n) / \log n \to \infty as n \to \infty

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

82.lean

Retained formal statement1 of 2

F(n)/log⁡n→∞asn→∞F(n) / \log n \to \infty as n \to \infty

FormalConjectures/ErdosProblems/82.leanErdos82.erdos_821 lineExact file
Filter.Tendsto (fun n => ↑(Erdos82.F n) / Real.log ↑n) Filter.atTop Filter.atTop
OpenStatement only, no proof