Pith. sign in

REVIEW 2 major objections 2 minor 18 references

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

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.3

2026-06-28 15:59 UTC pith:KTB5GYW6

load-bearing objection This paper runs a large-scale computational search on r_3(212) that rules out 44-sets in most subproblems via splitting and pruning but leaves two chunks unresolved and provides no explicit soundness proof for the reductions. the 2 major comments →

arxiv 2606.04016 v1 pith:KTB5GYW6 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
classification cs.LO
keywords r_3(N)3-AP-free setscomputational searchCP-SATupper bounds on arithmetic-progression-free setsDRAT proofs
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

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.

Watch this falsifier — get emailed when new claim-graph text bears on it.

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

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

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

0 comments
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.

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 ↗

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]

    arXiv preprint arXiv:2007.03528 , year=

    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