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
Is there a polynomial of degree at least and a set such that for any there is exactly one and such that ?
True ↔ ∃ f, 2 ≤ f.degree ∧ ∃ A, ∀ (z : ℤ), ∃! ab, ab ∈ A ×ˢ ((fun x => Polynomial.eval x f) '' {n | 0 < n}) ∧ z = ab.1 + ab.2OpenStatement only, no proof