Conjectures.io

Number theory

Erdős 324 - quintic

Probably f(x)=x5f(x) = x^5 has the property that the sums f(a)+f(b)f(a)+f(b) with a<ba < b nonnegative integers are distinct.

References

No one has attempted this yet.

Formal statement

Lean type

Set.InjOn
  (fun x =>
    match x with
    | (a, b) => a ^ 5 + b ^ 5)
  {(a, b) | a < b}

What you must prove

import FormalConjectures.ErdosProblems.«324»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos324.erdos_324.variants.quintic" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/324.lean

Source type SHA-256
sha256:946fff095619d97c20997ba5e2741224f3afc216f61ee495ffb293c048201243
Task id
fc-379fc029-variants-quintic-779286bfe4-formalized-v1
Task commitment
sha256:0ac270c9d169f02592e0e2a92e8234021bb9e6c046b461fc734009b993811e8a

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.