Erdős problem 13 - general

A general version asks, for a fixed

r \in \mathbb{N}

, if a set

A \subseteq \{1, ..., N\}

has no

a \in A

and

b_1, ..., b_r \in A

such that

a | (b_1 + ... + b_r)

and

a < \min(b_1, ..., b_r)

, then is it true that

|A| \le N/(r+1) + O(1)

$1,024 bounty

Solve it

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

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-variants-general-d96118aff1591ef8b6f38435-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«13»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos13.erdos_13.variants.general" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∀ (r : ℕ),
  ∃ C,
    ∀ (N : ℕ),
      ∀ A ⊆ Finset.Icc 1 N,
        (∀ a ∈ A, ∀ (b : Fin r → ℕ), (∀ (i : Fin r), b i ∈ A) → (∀ (i : Fin r), a < b i) → ¬a ∣ ∑ i, b i) →
          ↑A.card ≤ ↑N / (↑r + 1) + C

Original conjecture source: FormalConjectures/ErdosProblems/13.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:19fef883ead0ea7706b9c91b24373b3c84e6a2919042e2631dfe6c4d9b51b620
Task id: fc-v2-variants-general-d96118aff1591ef8b6f38435-formalized
Task commitment: sha256:d32836d1197512cbf77818d873b8a800b2654c85c79082fb4cf0682d3ce2ef69

References

erdosproblems.com/13

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord