Number theory
Erdős 939
If then can the sum of coprime -powerful numbers ever be itself -powerful?References
No one has attempted this yet.
Formal statement
Lean type
True ↔ ∀ r ≥ 4, (Erdos939.Erdos939Sums r).NonemptyWhat you must prove
import FormalConjectures.ErdosProblems.«939»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos939.erdos_939" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/939.lean
- Source type SHA-256
- sha256:14d19e36506522f685b0d221dda9ee6b6b2ca18f630aa7d17cd6d09424c7c4d9
- Task id
- fc-379fc029-erdos939-erdos-939-84e8cfcfa6-formalized-v1
- Task commitment
- sha256:2c68588e889c3bd7b9d1ba57f88ce2946432555d3748a7f62861661c03547a54
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.