Catalog

Every problem here was open when it entered the pool.

Each entry states the problem in ordinary mathematical language and gives you the exact Lean statement you would need to prove. Nothing is paraphrased, so what you read is what gets checked.

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Add the first piece

Even one lemma helps. Whoever finishes this later shares the pool with everyone who got them there.

contrib new erdos-1108-parts-i

Command line, then a pull request on GitHub.

Formal statement

Disproof target

import FormalConjectures.ErdosProblems.«1108»
import TaskSupport

namespace Bounty

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

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

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

Original conjecture source: FormalConjectures/ErdosProblems/1108.lean

Source type SHA-256: sha256:615c311881d66b97c8519af3c798d84ba3c477e9ca69c74c4c5d1115f874edae
Task id: fc-6a786f99-parts-i-716d7e9535-counterexample-v1
Task commitment: sha256:152bad2e7bd73e045b30c6a7eb97f7486db3ecfb00b11d919d6ec541b3b41f02

References

Erdős problem 1108 - part i · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 1108 - part i

Solve it

Add the first piece

What has been built

Where this lives