Erdős problem 477
Does there exist an integer polynomial of degree at least two and a set such that every integer has a unique representation ? A manuscript claims the thirteenth powers admit a tiling complement.
Sources
FormalConjectures/ErdosProblems/
477.lean
Retained formal statement
There is no such for the polynomial .
This is shown in [Sek59].
∀ (A : Set ℤ), ∃ z, ¬∃! a, a ∈ A ×ˢ ((fun x => Polynomial.eval x (Polynomial.X ^ 2)) '' {n | 0 < n}) ∧ z = a.1 + a.2SolvedStatement only, no proof