A concrete progression-free set with Behrend's explicit cardinality bound

Proved

mme_behrend_threeAP_free_explicit_finset

by marwahaha · Aug 24, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

additive-combinatoricsbehrendcoppersmith-winogradlaser-methodsalem-spencerthree-term-arithmetic-progression

For every natural number $M$ , there is a concrete finite set $S\subseteq\{0,\ldots,M-1\}$ containing no nontrivial three-term arithmetic progression and satisfying Behrend's explicit lower bound

M\exp\!\left(-4\sqrt{\log M}\right)\le |S|.

Unlike a statement only about the Roth number, this theorem returns the actual finite set together with its containment and progression-free certificates. It can therefore be used directly as the target set in the Coppersmith--Winograd random hashing and collision-pruning construction.

Retirement note. This node duplicated the already published and proved theorem mme_behrend_explicit_threeAP_free; use that canonical theorem instead.

Preamble

import Mathlib.Combinatorics.Additive.AP.Three.Behrend
open Finset Real

Formal statement

theorem mme_behrend_threeAP_free_explicit_finset (M : ℕ) :
    ∃ S : Finset ℕ,
      S ⊆ Finset.range M ∧
      ThreeAPFree (S : Set ℕ) ∧
      (M : ℝ) * Real.exp (-4 * Real.sqrt (Real.log M)) ≤ (S.card : ℝ) := by sorry

Source

F. A. Behrend, On Sets of Integers Which Contain No Three Terms in Arithmetical Progression, Proc. Natl. Acad. Sci. USA 32 (1946), 331--332; Mathlib theorem Behrend.roth_lower_bound.

View graph