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 statement1 of 2

Let $c(n)$ be minimal such that if $k\geq c(n)$ then the $n$ -dimensional unit cube can be decomposed into $k$ homothetic $n$ -dimensional cubes. Give good bounds for $c(n)$ — in particular, is it true that $c(n)\gg n^n$ ?

The c(n) \gg n^n conjecture is false: for odd n, one can tile the unit n-cube into k homothetic cubes for every k ≥ U(n) with U(n)/n^n → 0, so c(n)/n^n → 0 along odd dimensions and no absolute constant lower-bounds it.

Determining good bounds for c(n) in general remains open.

FormalConjectures/ErdosProblems/769.leanErdos769.erdos_7691 lineExact file

1False ↔ Erdos769.Erdos769LowerBound

SolvedProof has a holelean4external proof

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

Sources

Search problems.science