Number theory

Erdős 1108 - part i

For each

k \geq 2

, does the set

A = \left\{ \sum_{n\in S}n! : S\subset \mathbb{N}\text{ finite}\right\}

of all finite sums of distinct factorials contain only finitely many

k

-th powers?

References

erdosproblems.com/1108

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ k ≥ 2, {a | a ∈ Erdos1108.FactorialSums ∧ ∃ m, m ^ k = a}.Finite

What you must prove

import FormalConjectures.ErdosProblems.«1108»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1108.erdos_1108.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1108.lean

Source type SHA-256: sha256:2dee53b6faa8d3676ee111b2eb243b2145b0cd6066cab56218fa7ce45750f3a9
Task id: fc-379fc029-parts-i-102fdacae3-formalized-v1
Task commitment: sha256:909ae4f2ba4b970e81d0b6769e47e205dafff4759095bcd11c3b49bd7e46b8e9

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.