Erdős problem 170

The problem is to determine the limit of the sequence $\frac{F(N)}{\sqrt{N}}$ as $N \to \infty$ .

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

170.lean

Retained formal statement3 of 3

Sanity Check: the trivial ruler is actually a perfect ruler if $K \geq N$

FormalConjectures/ErdosProblems/170.leanErdos170.trivial_ruler_is_perfect1 lineExact file

1∀ (N : ℕ), Erdos170.TrivialRuler N ∈ Erdos170.PerfectRulersLengthN N

APIStatement only, no proof