Erdős problem 769 · problems.science

For the least cutoff $c(n)$ after which every $k$ occurs as the number of homothetic cubes in a decomposition of the unit $n$ -cube, is $c(n) \gg n^n$ ? The Lean proof shows $c(n) = o(n^n)$ along odd dimensions.

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

769.lean

Retained formal statement2 of 2

What refuting $c(n)\gg n^n$ leaves open: give good bounds for $c(n)$ . Asked here on the scale the problem itself sets, $n^n$ : does $c$ have a well-defined order $\lim_{n\to\infty}\frac{\log c(n)}{n\log n}?$ The refuted conjecture would have forced this limit to be at least $1$ .

FormalConjectures/ErdosProblems/769.leanErdos769.erdos_769.variants.growth_rate4 linesExact file

1True ↔2  ∃ c,3    (∀ (n : ℕ), Erdos769.IsCutoff n (c n)) ∧4      ∃ γ, Filter.Tendsto (fun n => Real.log ↑(c n) / (↑n * Real.log ↑n)) Filter.atTop (nhds γ)

OpenStatement only, no proof

Sources

Search problems.science