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

Open selected source

FormalConjectures/ErdosProblems/

1084.lean

Retained formal statement5 of 5

Erdős claims the existence of two constants $c_1, c_2 > 0$ such that $6n - 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

1∃ c₁,2  ∃ c₂ > 0,3    ∀ᶠ (n : ℕ) in Filter.atTop,4      6 * ↑n - c₁ * ↑n ^ (2 / 3) ≤ ↑(Erdos1084.f 3 n) ∧ ↑(Erdos1084.f 3 n) ≤ 6 * ↑n - c₂ * ↑n ^ (2 / 3)

SolvedStatement only, no proof

Sources

Search problems.science