Non-dividing sets and the extremal function $F(N)$ of Erdős problem #131

Definition

Erdos131_NonDividing

by moutei · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatoricserdos-problemsnumber-theory

A finite set $A\subseteq\mathbb{N}$ is called non-dividing when no element of $A$ divides the sum of any nonempty subset of the remaining elements:

\forall a\in A,\ \forall\, \emptyset\neq S\subseteq A\setminus\{a\},\qquad a\nmid\sum_{x\in S}x.

Singleton subsets are included, so a non-dividing set is in particular primitive: taking $S=\{b\}$ forbids $a\mid b$ for distinct $a,b\in A$ . The subset $S$ is required to be nonempty because the empty sum is $0$ , which every $a$ divides; allowing $S=\emptyset$ would make the property unsatisfiable.

$F(N)$ is the extremal function of the problem: the largest cardinality of a non-dividing subset of $\{1,\ldots,N\}$ . Erdős asks for its order of growth. The known bounds are $N^{1/5}\ll F(N)\le N^{1/4+o(1)}$ , the lower bound due to Csaba and the upper bound a consequence of the result of Pham and Zakharov on non-averaging sets; Erdős, Lev, Rauzy, Sándor and Sárközy proved the explicit bound $F(N)<3N^{1/2}+1$ . The correct growth rate is open.

Formalization Note. The forbidden subsets are drawn from A.erase a, so the tested element never occurs in the sum it is tested against. Membership in (A.erase a).powerset is definitionally the subset relation, and is written that way so the property is decidable, which is what allows an explicit finite witness to be checked by the Lean kernel.

Definition code

import Mathlib.Tactic
import Mathlib.Data.Finset.Sort
import Mathlib.Data.ZMod.Basic

namespace Erdos131

/-!
Erdős problem #131 (Erdős, Lev, Rauzy, Sándor and Sárközy call the property
*non-dividing*).

A finite set `A` of naturals is **non-dividing** when no element of `A` divides the sum of any
nonempty subset of the *other* elements. Two modelling points.

* The forbidden subsets are drawn from `A.erase a`, so `a` itself never appears in the sum it is
  tested against. Singleton subsets are included, so `NonDividing A` already forces `A` to be
  primitive: `a ∣ b` is the case `S = {b}`.
* The subset must be nonempty. The empty sum is `0`, which every `a` divides, so allowing `S = ∅`
  would make the property unsatisfiable.
* Membership `S ∈ (A.erase a).powerset` is definitionally `S ⊆ A.erase a`; it is written this way
  so that the property is decidable, which is what lets a finite witness be checked by the kernel.

`F N` is the extremal function of the problem: the largest size of a non-dividing subset of
`{1, …, N}`. Erdős asks for its growth rate; the known bounds are
`N ^ (1/5) ≪ F N ≤ N ^ (1/4 + o(1))`, and the truth is unknown.
-/

/-- No element of `A` divides the sum of any nonempty subset of `A` not containing it. -/
def NonDividing (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, ∀ S ∈ (A.erase a).powerset, S.Nonempty → ¬ (a ∣ ∑ x ∈ S, x)

/-- `NonDividing` is a decidable property: both quantifiers range over finite sets and
divisibility of naturals is decidable. This is what lets the kernel check an explicit witness. -/
instance (A : Finset ℕ) : Decidable (NonDividing A) := by
  unfold NonDividing; infer_instance

/-- The non-dividing subsets of `{1, …, N}`. -/
def IsNDIn (N : ℕ) (A : Finset ℕ) : Prop :=
  A ⊆ Finset.Icc 1 N ∧ NonDividing A

/-- `F N` is the maximal size of a non-dividing subset of `{1, …, N}`: the function Erdős
problem #131 asks us to estimate. -/
def F (N : ℕ) : ℕ :=
  ((Finset.Icc 1 N).powerset.filter (fun A => NonDividing A)).sup Finset.card

end Erdos131

Source

https://www.erdosproblems.com/131 — Erdős problem #131; P. Erdős, V. Lev, G. Rauzy, C. Sándor, A. Sárközy, 'Greedy algorithm, arithmetic progressions, subset sums and divisibility', Discrete Math. 200 (1999); also problem C16 in R. K. Guy, 'Unsolved Problems in Number Theory', 3rd ed. (2004).

View graph

Non-dividing sets and the extremal function F(N)F(N)F(N) of Erdős problem #131

Non-dividing sets and the extremal function $F(N)$ of Erdős problem #131