Field theory and polynomials

Erdős 477 - monomial

Probably there is no such

A

for the polynomial

X^k

for any

k \ge 2

. This is asked in [Sek59].

References

erdosproblems.com/477

Sek59 Milan Sekanina, Замечания к фактoризации беcкoнечнoй цикличеcкoй группы, Czechoslovak Mathematical Journal, Vol. 9 (1959), No. 4, 485–495

No one has attempted this yet.

Formal statement

Lean type

∀ (k : ℕ),
  2 ≤ k → ∀ (A : Set ℤ), ∃ z, ¬∃! a, (a ∈ A ×ˢ Set.range fun x => Polynomial.eval x (Polynomial.X ^ k)) ∧ z = a.1 + a.2

What you must prove

import FormalConjectures.ErdosProblems.«477»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos477.erdos_477.variants.monomial" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/477.lean

Source type SHA-256: sha256:1e6a688779bfee53b7e5e2c4b678eb8ca0afb780bcfbdf327c2def1986076ff7
Task id: fc-379fc029-variants-monomial-cf7da87986-formalized-v1
Task commitment: sha256:da7f17175958fcb43ded55e18cf94c9eaa1e744151a6c3c719ac530c45090a66

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.