Witness-split + window-cardinality refinement for $r_3(N)$: Architecture, empirical results, and a structural hard pocket
Mehmet Ergezer
cs.LO
May 31, 2026 · v1
TL;DR
Releases a Lean formal-proof-search encoding of the two resistant subproblems from an upper-bound search on r_3(212).
Abstract
We describe a reproducible computational framework for upper-bound searches on r_3(N), the maximum size of a 3-term-arithmetic-progression-free subset of [1,N]. The framework combines a verified lower-bound witness, endpoint forcing, depth-d witness-variable splitting, OEIS A003002 window-cardinality pruning, and recursive refinement of timed-out subproblems. Applied to the frontier case N = 212, K = 44, it found no feasible 44-set across millions of CP-SAT subproblems, supporting but not proving the conjectural value r_3(212) = 43. A 300-second recap leaves 45 resistant chunks; one-hour HiGHS MIP closes none of them; the full eight-hour HiGHS audit closes 25/45 and leaves 20/45 with dual bounds still pinned at 0.0. A CDCL/SAT re-attack on those LP-paradigm-resistant chunks closes 18 via conflict-driven clause learning; all eighteen carry independently verified DRAT proofs. The remaining two chunks (T1c) resist every tested paradigm under generous wall caps. We release the witness, solver scripts, result logs, tiered benchmark instances, verified DRAT/LRAT proofs, and a Lean formal-proof-search encoding of T1c, and frame the unit-gap problem r_3(212) in {43,44} as a target for stronger additive-combinatorial bounds, custom branch-and-bound, or formal proof-search systems.
Problem
Determining the exact value of r_3(N), the maximum size of a 3-term-arithmetic-progression-free subset of [1,N], is computationally hard at the frontier. The next open case is N=212, where it is unknown whether r_3(212)=43 or 44.
Approach
The authors build a reproducible CP-SAT framework combining a verified 43-element lower-bound witness, endpoint forcing, depth-24 witness-variable splitting, OEIS A003002 window-cardinality pruning, and recursive refinement of timed-out subproblems. Millions of CP-SAT subproblems are generated and attacked with CP-SAT, HiGHS MIP, and CDCL/SAT solvers. DRAT/LRAT proofs are independently verified for closed chunks, and a Lean formal-proof-search encoding is released for the two remaining resistant chunks (T1c).
Results
Zero feasible 44-sets were found across millions of subproblems, providing strong empirical support for r_3(212)=43 but not a formal proof. Window-cardinality pruning reduced the UNKNOWN rate from 30% to 1.65-6.07%. Two chunks resist every tested paradigm and are released as benchmark instances alongside a Lean encoding.
| Range | Chunks | UNK without bounds | UNK with bounds | Reduction |
|---|
| [575, 675) | 100 | 27.00% | 0.00% | -27.0 pp |
| [1575, 11575) | 10,000 | 30.33% | 1.65% | -28.7 pp |
| [11575, 111575) | 100,000 | n/a | 6.07% | -- |
Window-cardinality pruning effect
