Number theory · Last catalog review 26 Jul 2026

Erdős Problem 1107

Let

r \ge 2

. Is every large integer the sum of at most

r + 1

many

r

-powerful numbers?

References

Published 24 Jun 2026Never attempted

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-e923379e-erdos1107-erdos-1107-f46e9bf10e-formalized-v1
Task commitment: sha256:9f5231a04072070da6580d3f9dacf6bfb07578ac144323231e5c9886f710c78d

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.