Prove2Me

The base case: a cube-free subset of Z/8Z\mathbb{Z}/8\mathbb{Z} has at most five elements

Proved
Z2nFiveEighths.cubeFree_mod_eight_card_le_five

by aarontcao · Sep 17, 2026 · Mathlib 0df444a (Lean v4.33.1)

additive-combinatoricscombinatorics

Every cube-free A⊆Z/8ZA \subseteq \mathbb{Z}/8\mathbb{Z} has ∣A∣≤5|A| \le 5.

A finite check over all 28=2562^8 = 256 subsets. The bound is attained by {1,3,4,5,7}\{1, 3, 4, 5, 7\}, which is the mod-8 shadow of the extremal construction, so it is sharp and not slack.

Preamble
import Mathlib
import Definitions.Def_Z2nCubeFreeLayers
Formal statement
namespace Z2nFiveEighths

theorem cubeFree_mod_eight_card_le_five (A : Finset (ZMod 8)) (hA : CubeFree A) :
    A.card ≤ 5 := by sorry

end Z2nFiveEighths
Source
Jason Long and Adam Zsolt Wagner, "The largest projective cube-free subsets of Z_{2^n}", arXiv:1810.01225, https://arxiv.org/abs/1810.01225, the n=3n = 3 case of Conjecture 5.1
Read-back

What the Lean code literally says, in plain math · claude-opus-5

READ-BACK

Call a finite subset A of an additive abelian group "rich" if there exist elements x, y, z of the group, not required to be distinct, such that all seven of x, y, z, x+y, y+z, z+x, x+y+z lie in A. Equivalently, A contains all seven nonempty subset sums of some triple (with repetition allowed) of its own elements. The theorem asserts: every finite subset A of the cyclic group of residues mod 8 that is not rich has at most 5 elements. The inequality is non-strict, and 5 is a fixed numeral, not an existentially quantified constant, sitting inside an ambient group of order 8. The proof body is a placeholder (sorry), so only the statement is at stake.

QUANTIFIER ORDER

  1. G: any type carrying an additive abelian group structure (used only by the two definitions).
  2. A: a finite subset of G, universally quantified; the existential below sits inside its scope.
  3. x, y, z: existentially quantified over all of G, jointly, with the seven memberships conjoined under that single existential. The first three conjuncts force them into A.
  4. In the target, A is a universally quantified finite subset of Z/8Z, then the hypothesis, then the cardinality claim.

HYPOTHESES AddCommGroup G: commutativity makes the three pairwise sums unordered, and associativity makes x+y+z unambiguous (parsed as (x+y)+z). Z/8Z satisfies it. hA: A is not rich. It rules out every triple drawn from A, repeats allowed, whose seven subset sums all land in A. Two consequences of allowing repeats: taking x=y=z=0 shows 0 cannot be in A, so A misses the identity and |A| is at most 7 already; taking x=y=z=a shows no a in A has both 2a and 3a in A. Nothing requires A nonempty, or closed, or symmetric.

DEGENERATE CASES A empty satisfies the hypothesis vacuously and gives 0 <= 5. The hypothesis is therefore satisfiable and the statement is not vacuous. Singletons such as {1} also satisfy it. Because the ambient group has 8 elements and the hypothesis already excludes 0, the conclusion carries content only for A of size 6 or 7: it says no 6-element set of nonzero residues mod 8 avoids the configuration. x, y, z quantify over all of G rather than over A, but the first three conjuncts pin them to A, so nothing outside A can witness richness.

UNREADABLE nothing

Human review

  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by aarontcao · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph