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 statement2 of 5

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

Note: in [Er75f] is read $9n^2 + 6n$ , but this seems to be a typo.

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

1∀ {n : ℕ}, Erdos1084.f 2 (3 * n ^ 2 + 3 * n + 1) = 9 * n ^ 2 + 3 * n

OpenStatement only, no proof