pith. sign in

arxiv: 2606.04016 · v1 · pith:KTB5GYW6new · submitted 2026-05-31 · 💻 cs.LO

Witness-split + window-cardinality refinement for r₃(N): Architecture, empirical results, and a structural hard pocket

Mehmet Ergezer This is my paper

Pith reviewed 2026-06-28 15:59 UTC · model grok-4.3

classification 💻 cs.LO
keywords r_3(N)3-AP-free setscomputational searchCP-SATupper bounds on arithmetic-progression-free setsDRAT proofs
0
0 comments X

The pith

A computational framework rules out all 44-element 3-AP-free subsets of [1,212]

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a reproducible solver that combines witness splitting, endpoint forcing, window-cardinality pruning, and recursive refinement to search for large 3-AP-free sets. When applied to the open case N=212 and target size 44, the method processes millions of subproblems and reports no solutions. This outcome is consistent with the conjecture that the maximum size is 43, narrowing the remaining unit gap without a full proof. All scripts, instances, and verified DRAT proofs are released so others can inspect or extend the search.

Core claim

The framework applied to N=212 and K=44 finds no feasible 44-set across millions of CP-SAT subproblems, supporting the conjectural value r_3(212)=43 while leaving two resistant chunks that resist both MIP and CDCL attacks.

What carries the argument

Depth-d witness-variable splitting together with OEIS A003002 window-cardinality pruning

If this is right

  • r_3(212) is at most 43
  • The unit-gap question is now reduced to proving that no 44-set exists
  • The two remaining resistant chunks become explicit targets for stronger combinatorial bounds or new proof-search systems

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Analytic upper-bound techniques from additive combinatorics could be tested directly against the released resistant instances
  • The pattern of solver resistance may indicate a structural property of the remaining chunks that current LP and clause-learning methods miss

Load-bearing premise

The window-cardinality pruning rules and depth-d witness splitting never discard a valid 44-set.

What would settle it

Existence of even one 44-element subset of [1,212] with no three-term arithmetic progression would falsify the reported search result.

Figures

Figures reproduced from arXiv: 2606.04016 by Mehmet Ergezer.

Figure 1
Figure 1. Figure 1: Funnel from the retained ‘100k‘ broad expansion batch to the final two￾chunk T1c residual. T1 is a ‘45‘-chunk subset produced by recapping a uniform random ‘100‘-chunk sample of the ‘6,071‘ broad UNKNOWN chunks at ‘300‘ seconds. Both controlled A/Bs show a roughly 28-percentage-point reduction in UNK rate at the 60-s broad wall cap. The window-bound family is strictly stronger than the baseline 3-AP family… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper presents a reproducible computational framework for upper bounds on r_3(N) that integrates verified lower-bound witnesses, endpoint forcing, depth-d witness-variable splitting, OEIS A003002 window-cardinality pruning, and recursive refinement of timed-out subproblems. For the frontier instance N=212 and K=44 the search over millions of CP-SAT subproblems reports no feasible 44-set; 18 of 45 resistant chunks are closed by CDCL with independently verified DRAT proofs, while two T1c chunks remain resistant under all tested paradigms and are supplied with a Lean formal-proof-search encoding. The manuscript frames the unit-gap question r_3(212) ∈ {43,44} as a target for stronger combinatorial bounds or automated proof systems.

Significance. If the splitting and pruning reductions are solution-preserving, the negative search result supplies substantial computational evidence supporting the conjecture r_3(212)=43. The public release of the witness, solver scripts, logs, DRAT/LRAT proofs, tiered benchmark instances, and Lean encoding constitutes a concrete, reusable artifact that can accelerate independent verification and further work at the interface of additive combinatorics and automated reasoning.

major comments (2)
  1. [Abstract] Abstract and framework description: the claim that 'no feasible 44-set' was found rests on depth-d witness-variable splitting and OEIS A003002 window-cardinality pruning never discarding a valid 3-AP-free 44-subset of [1,212]. No invariant, small-case verification, or formal argument establishing solution preservation is supplied; this is load-bearing because an unsound reduction would make the negative outcome inconclusive rather than supportive.
  2. [Results section (resistant chunks)] Results on resistant chunks: after the 300-second recap leaves 45 chunks, the subsequent HiGHS and CDCL closures are reported, yet the text does not quantify how the initial pruning affects coverage of the original search space. Without this accounting it is unclear whether the two remaining T1c instances represent the full problem or an already-reduced subproblem.
minor comments (2)
  1. [Abstract] The term 'recap' in the abstract would benefit from a parenthetical reference to the subsection that defines the 300-second timeout and chunking procedure.
  2. A compact table summarizing closure counts (CP-SAT, HiGHS, CDCL) and proof status across the 45 chunks would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for explicit soundness arguments and coverage accounting. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract and framework description: the claim that 'no feasible 44-set' was found rests on depth-d witness-variable splitting and OEIS A003002 window-cardinality pruning never discarding a valid 3-AP-free 44-subset of [1,212]. No invariant, small-case verification, or formal argument establishing solution preservation is supplied; this is load-bearing because an unsound reduction would make the negative outcome inconclusive rather than supportive.

    Authors: We agree that the manuscript lacks an explicit invariant, small-case verification, or consolidated formal argument for solution preservation of the two reductions, and that this is a substantive gap for a load-bearing claim. The splitting enumerates all assignments to the depth-d witness variables (hence partitions the space), and the window pruning applies known maximal cardinalities from A003002, but these properties are only described informally. We will add a dedicated subsection to the framework description that states the preservation invariants, supplies a short inductive argument for the splitting, notes that A003002 bounds are exhaustive for the relevant window sizes, and includes a small-N verification (N ≤ 30) where the reduced search reproduces the known r_3 values. revision: yes

  2. Referee: [Results section (resistant chunks)] Results on resistant chunks: after the 300-second recap leaves 45 chunks, the subsequent HiGHS and CDCL closures are reported, yet the text does not quantify how the initial pruning affects coverage of the original search space. Without this accounting it is unclear whether the two remaining T1c instances represent the full problem or an already-reduced subproblem.

    Authors: The 45 chunks are produced after the complete depth-d splitting and window-cardinality pruning have been applied during the 300-second recap; they therefore already lie in the reduced search space. Because both reductions are solution-preserving, any 44-set that existed in the original instance would survive into one of these chunks. We will revise the results section to include a short paragraph and table that (a) states the fraction of the original search tree pruned by the window-cardinality bounds and (b) confirms that the two T1c instances are the only remaining open subproblems after exhaustive enumeration of all pruned branches, thereby representing the unresolved portion of the original problem. revision: yes

Circularity Check

0 steps flagged

No circularity; result from external solvers on reduced instances

full rationale

The paper presents a computational search using CP-SAT, HiGHS MIP, and CDCL solvers on subproblems generated by witness splitting and OEIS-derived cardinality bounds. No equations, parameters, or derivations are defined in terms of the target result r_3(212). No self-citations are load-bearing for the central claim. The outcome (no 44-set found) is produced by running independent solvers rather than by any internal fit or renaming. Soundness of the reductions is a separate verification question outside the circularity criteria.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The framework rests on the assumption that standard CP-SAT and MIP solvers return correct unsatisfiability results on the generated instances and that the OEIS-derived window-cardinality bounds are sound for the pruning step; no free parameters are introduced in the abstract.

axioms (2)
  • domain assumption Standard CP-SAT and MIP solvers correctly decide the generated sub-instances.
    Invoked when the abstract reports that millions of subproblems were solved with no feasible 44-set.
  • domain assumption OEIS A003002 window-cardinality pruning never discards a valid solution.
    Used to reduce the search space before solver calls.

pith-pipeline@v0.9.1-grok · 5808 in / 1421 out tokens · 30840 ms · 2026-06-28T15:59:20.700271+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

18 extracted references · 4 canonical work pages · 1 internal anchor

  1. [1]

    and Spencer, D

    Salem, R. and Spencer, D. C. , title =. Proceedings of the National Academy of Sciences , year =

  2. [2]

    Behrend, F. A. , title =. Proceedings of the National Academy of Sciences , year =

  3. [3]

    Roth, K. F. , title =. Journal of the London Mathematical Society , year =

  4. [4]

    and Sisask, Olof , title =

    Bloom, Thomas F. and Sisask, Olof , title =. arXiv preprint , year =. 2007.03528 , archivePrefix =

    work page arXiv 2007

  5. [5]

    Kelley and R

    Kelley, Zander and Meka, Raghu , title =. arXiv preprint , year =. 2302.05537 , archivePrefix =

    work page arXiv

  6. [6]

    2024 , url =

    The On-Line Encyclopedia of Integer Sequences, sequence. 2024 , url =

    2024

  7. [7]

    2024 , publisher =

    Perron, Laurent and Furnon, Vincent , title =. 2024 , publisher =

    2024

  8. [8]

    and Hall, J

    Huangfu, Q. and Hall, J. A. J. , title =. Mathematical Programming Computation , year =. doi:10.1007/s12532-017-0130-5 , note =

    work page doi:10.1007/s12532-017-0130-5

  9. [9]

    Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions , series =

    Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Heisinger, Maximilian , title =. Proceedings of SAT Competition 2020: Solver and Benchmark Descriptions , series =. 2020 , pages =

    2020

  10. [10]

    SAT 2018 , pages =

    Ignatiev, Alexey and Morgado, Antonio and Marques-Silva, Joao , title =. SAT 2018 , pages =. 2018 , doi =

    2018

  11. [11]

    Heule, Marijn J. H. and Hunt, Jr., Warren A. and Biere, Armin , title =. FMCAD 2013 , year =

    2013

  12. [12]

    Efficient Certified

    Cruz-Filipe, Lu. Efficient Certified. CADE-26 , year =

  13. [13]

    Advancing Mathematics Research with AI-Driven Formal Proof Search

    Tsoukalas, George and Kovsharov, Anton and Shirobokov, Sergey and Surina, Anja and Firsching, Moritz and B. Advancing Mathematics Research with. arXiv preprint , year =. 2605.22763 , archivePrefix =

    work page internal anchor Pith review Pith/arXiv arXiv

  14. [14]

    formal-conjectures: A Lean library of open mathematical conjectures , year =

  15. [15]

    CPP 2020 , year =

    The. CPP 2020 , year =

    2020

  16. [16]

    CADE-28 , year =

    de Moura, Leonardo and Ullrich, Sebastian , title =. CADE-28 , year =

  17. [17]

    2024 , howpublished =

    Cariboni, Lorenzo , title =. 2024 , howpublished =

    2024

  18. [18]

    2026 , howpublished =

    Ergezer, Mehmet , title =. 2026 , howpublished =

    2026