Conjectures.io

Field theory and polynomials

Erdős 477 - X pow three

Probably there is no such AA for the polynomial X3X^3.

References

  • 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

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

What you must prove

import FormalConjectures.ErdosProblems.«477»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/477.lean

Source type SHA-256
sha256:6b92749cc0b4a99fc7d402a7918889949b99f7e50709bd13e5546219d03dea46
Task id
fc-379fc029-variants-x-pow-three-f045d570a6-formalized-v1
Task commitment
sha256:f278c242bb7374eee87d73a878784a6b1e1e0fac3bdb25131040a70b03828e62

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.