Conjectures.io

Combinatorics

Erdős 241 - generalization

More generally, Bose and Chowla [BoCh62] conjectured that the maximum size of A⊆{1,…,N}A\subseteq \{1,\ldots,N\} with all rr-fold sums distinct (aside from the trivial coincidences) then ∣A∣∼N1/r.\lvert A\rvert \sim N^{1/r}.

References

  • [BoCh62] Bose, R. C. and Chowla, S., Theorems in the additive theory of numbers. Comment. Math. Helv. (1962/63), 141-147.
  • [Gr01] Green, Ben, The number of squares and {$Bh[g]$} sets. Acta Arith. (2001), 365-390.
  • [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.

No one has attempted this yet.

Formal statement

Lean type

∀ r ≥ 2, Erdos241.BoseChowlaConjecture r

What you must prove

import FormalConjectures.ErdosProblems.«241»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos241.erdos_241.variants.generalization" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/241.lean

Source type SHA-256
sha256:1361871c955c79452f93d0ec881d9afe2a33ef785e25423354c6289bd6c3fda3
Task id
fc-379fc029-variants-generalization-ecb986268b-formalized-v1
Task commitment
sha256:0e6aacfda33c0ca5dfe1ab662ad8e7213109da2cf2aa8e366917622884c5b067

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.