Erdős problem 1084

Erdős conjectured that the triangular lattice is best possible in 2D, in particular that $f_2(3n^2 + 3n + 1) < 9n^2 + 3n$ .

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1084.lean

Retained formal statement4 of 5

Erdős showed that there is some constant $c > 0$ such that $f_2(n) < 3n - c n^{1/2}$ .

FormalConjectures/ErdosProblems/1084.leanErdos1084.erdos_1084.variants.upper_d21 lineExact file

1∃ c > 0, ∀ n > 0, ↑(Erdos1084.f 2 n) < 3 * ↑n - c * √↑n

SolvedStatement only, no proof