Conjectures.io

Number theory

Erdős 1107

Let r≥2r \ge 2. Is every large integer the sum of at most r+1r + 1 many rr-powerful numbers?

References

  • He88

No one has attempted this yet.

Formal statement

Lean type

∀ r ≥ 2, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos1107.SumOfRPowerful r n

What you must prove

import FormalConjectures.ErdosProblems.«1107»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1107.erdos_1107" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1107.lean

Source type SHA-256
sha256:7d3f25595511760c3b8766591417c5ee5db47667b52adbf48af1d8e4aad5d229
Task id
fc-379fc029-erdos1107-erdos-1107-baf513878f-formalized-v1
Task commitment
sha256:7d9b0c3e85e10d7463cdf5dee73b4747ff2b968a73ce2f2f7b7f31436964a614

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.