TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Every nonempty finite set of $n$ nonzero integers has a sum-free subset of size greater than $n / 3$

Statement

Every nonempty finite set $A$ of $n$ nonzero integers contains a sum-free subset of cardinality strictly greater than $n / 3$ .

Facts & Assumptions

Given: A nonempty finite set $A \subseteq Z ∖ {0}$ with $∣ A ∣ = n$ .

[L1]

Sum-free means no three members, with repeated summands allowed, satisfy $x + y = z$ (Sum-free subsets of the integers).

[L2]

There are primes $p$ arbitrarily large with $p \equiv 2 (m o d 3)$ (There are arbitrarily large primes congruent to $2$ modulo $3$ ).

[L3]

For prime $p$ , nonzero residue classes form the multiplicative group of the field $Z / p$ (For every prime $p$ , the two operations on $Z / p$ make it a field).

[L4]

A nonempty finite set of real numbers has a maximum (Every nonempty finite set of reals has a maximum and a minimum).

[L5]

Uniform probabilities are cardinality ratios; indicators count membership, expectation is linear, and some outcome reaches at least the expectation (The uniform probability space on a nonempty finite set, Indicators turn event probabilities, intersections, and finite counts into expectations and products, Expectation is linear for every finite family of random variables, without any independence hypothesis, Expectation preserves pointwise order and lies between the minimum and maximum attained values).

Proof

technique · constructive

1.1

Since $A$ is nonempty, $n \geq 1$ . Choose a prime $p = 3 r + 2$ larger than twice $\max_{a \in A} ∣ a ∣$ .

givenL2L4chooseconstruct

1.2

Let $I = {r + 1, \dots, 2 r + 1} \subset Z / p$ . This set is sum-free modulo $p$ : if representatives $x, y, u \in I$ satisfied $x + y \equiv u (m o d p)$ , then $x + y - u$ would be a multiple of $p$ lying between $1$ and $3 r + 1 = p - 1$ , which is impossible.

L1algebra

2.1

Choose $z$ uniformly from the nonzero residue classes and put $B_{z} = {a \in A : z a m o d p \in I}$ . Reduction modulo $p$ is injective on $A$ by the choice of $p$ , and multiplication by each nonzero $a$ permutes the nonzero classes by [L3].

step 1.1L3

3.1

Thus every $a \in A$ belongs to $B_{z}$ with probability $∣ I ∣ / (p - 1) = (r + 1) / (3 r + 1) > 1 / 3$ . Linearity gives $E [∣ B_{z} ∣] = n (r + 1) / (3 r + 1) > n / 3$ .

step 2.1L5algebra

4.1

Some $z$ has $∣ B_{z} ∣$ at least the expectation. If $x + y = u$ in $B_{z}$ , then $z x + z y = z u$ modulo $p$ , contradicting sum-freeness of $I$ ; so $B_{z}$ is sum-free and has size greater than $n / 3$ .

step 1.2step 3.1L1L5discharge-construct∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. Bucic, Probabilistic Method, Theorem 2.3 (standard reference, not scraped)

Every nonempty finite set of nn nonzero integers has a sum-free subset of size greater than n/3n/3