Skip to content

Erdős problem 1084

Start work

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

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1084.lean

Retained formal statement5 of 5

Erdős claims the existence of two constants c1,c2>0c_1, c_2 > 0 such that 6n−c1n2/3≤f3(n)≤6n−c2n2/36n - c_1 n^{2/3} ≤ f_3(n) \le 6n - c_2 n^{2/3}.

FormalConjectures/ErdosProblems/1084.leanErdos1084.erdos_1084.variants.upper_lower_d34 linesExact file
∃ c₁,  ∃ c₂ > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      6 * ↑n - c₁ * ↑n ^ (2 / 3) ≤ ↑(Erdos1084.f 3 n) ∧ ↑(Erdos1084.f 3 n) ≤ 6 * ↑n - c₂ * ↑n ^ (2 / 3)
SolvedStatement only, no proof