Erdős problem 1084 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

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