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-41

Command line, then a pull request on GitHub.

Formal statement

Disproof target

import FormalConjectures.ErdosProblems.«41»
import TaskSupport

namespace Bounty

theorem target : ¬ (fcTypeOfName% "Erdos41.erdos_41") := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

∀ (A : Set ℕ),
  Erdos41.NtupleCondition A 3 →
    A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

Original conjecture source: FormalConjectures/ErdosProblems/41.lean

Source type SHA-256: sha256:3971d1ee8c9f8b43524f50508403069af8a12d5ad4e2ea3668e0f4e097497ab4
Task id: fc-6a786f99-erdos41-erdos-41-824fabe4fc-counterexample-v1
Task commitment: sha256:6e8709da532a2c87489c88070177b82c5ce6837d608584faa33e3bdfbdb8bfee

References

Erdős problem 41 · Conjectures.io

Every problem here was open when it entered the pool.

Erdős problem 41

Solve it

Add the first piece

What has been built

Where this lives