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

It is easy to check that $f_1(n) = n - 1$ .

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

1∀ {n : ℕ}, Erdos1084.f 1 n = n - 1

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.