Exact values for a finite Ramsey-type problem from Green's list (Problem 22): N_0(1)=9, N_0(2)=54, N_0(3)=774
Citable version that has not completed AIRR screening. Not peer reviewed. Screening record
For r >= 1 let N_0(r) be the least N such that every r-colouring of {1,...,N} contains x,y >= 3 (not necessarily distinct) with x+y and xy in {1,...,N} and of the same colour. This is the quantity in Problem 22 of Green's list of open problems. Using SAT solving I find N_0(1)=9, N_0(2)=54 and N_0(3)=774. The lower bounds N_0(r)>N come from explicit colourings, checked by independent programs including Lean 4. The upper bounds come from unsatisfiability of the corresponding CNF formulas; for r=2,3 this is supported by four solvers, two encodings and DRUP proofs checked by a small checker written for this note. It is not a formally verified proof, and the note is a small computational datum, not progress on the asymptotic question.
Preview PDF on this page v1
Uses your browser's PDF viewer. Open the PDF directly if a preview is unavailable.
Cite this paper
Lluis Eriksson (2026). Exact values for a finite Ramsey-type problem from Green's list (Problem 22): N_0(1)=9, N_0(2)=54, N_0(3)=774. AIRR.SCIENCE, ARR-2026-4CFDWEQNKA9F69BX, v1. https://airr.science/papers/ARR-2026-4CFDWEQNKA9F69BX/versions/v1/ Research preprint; ARR-2026-4CFDWEQNKA9F69BX v1. Not peer reviewed by AIRR. Working paper; not admitted to the AIRR accepted collection.
Use this version link to cite the manuscript you read. A Working paper label means the version has not completed AIRR screening. AIRR screening is not journal peer review. Import BibTeX, RIS or CSL JSON into your reference manager to apply a citation style.
Version history
The paper identifier remains stable. Each version has its own immutable release, timestamp and version identifier.
- v1 · source snapshot available · viewing
Verification record
- Frontier-model screening
- Not assessed
- Source integrity
- Pass
- Bibliographic integrity
- Not assessed
- Reproducibility
- Not assessed
- Lean 4
- Not assessed
Recorded under ARR-VERIFY-1.0. AIRR verification and screening are not peer review.
AI assistance statement
Substantial AI assistance (OpenAI Codex and Claude in research, proofs, drafting, computational checks and packaging) with Lluis Eriksson as author. No exact full-text assessment of this PDF exists; no score is claimed or entered in the public aggregate. No independent human peer review, formal verification or worldwide priority certification is claimed.
Frontier-model screening
Status: not_assessed. Any listed reports correspond to this exact version under ARR-SCREEN-1.0; no absent assessment is represented as a pass.
Model assessments and review context
- Distinct models
- 2
- Range
- 2.00–2.40
- Method
- bounded capability-weighted mean · exact version only
Limited evidence · 0/2 benchmark matches. This is an evidence description, not a probability of correctness.
One provider; shared blind spots possible; Fresh blinded review context not documented for every model; Benchmark match incomplete; Adverse reports or unresolved objections require editorial disposition
Review input clarification
Independent-thread note, 22 October 2026, by the author's Claude research session (not independent of the author). Claude Sonnet 5.5 report (2.00, minor_revision) made in an independent Claude Code thread: new session whose working folder held only paper.pdf and the instructions; the session reports that the user's global CLAUDE.md, a memory-directory notice and the launching message (naming the AIRR project) were loaded, that it knew nothing of the manuscript's content, and that it cannot certify context isolation (self-declared; disk access was not technically blocked). It is a non-human report from the same model family as the author's session. review_context and runtime_provenance are omitted because the schema admits no honest basis; the controls file is retained with its sha256 in registry/assessment-evidence/2026-10-22-claude-threads/. Model JSON preserved unedited; only the placeholder paper and version ids were filled. No other report exists for this version. No cost or tokens recorded.
Operator record · · Source files and affected reports
Review input clarification
Independent-thread note, 22 October 2026, by the author's Claude research session (not independent of the author). Claude Haiku 5.5 report (2.40, major_revision, independence 'not_involved_in_manuscript' as the model reported), non-human, from an independent Claude Code thread: new session with only paper.pdf and the instructions in its folder; it reports that the user's global CLAUDE.md, a memory-directory notice, linked-session names and the launching message were loaded (no memory file, shared notes or other report opened) and that it cannot verify context isolation. review_context and runtime_provenance omitted (no honest basis in the schema); controls file retained with sha256 in registry/assessment-evidence/2026-10-22-claude-threads-haiku/. Model JSON unedited; only placeholder ids filled. A separate base model from the Sonnet 5.5 thread report on the same version, which it does not replace. Reviewer's one unresolved material objection: the exact value N0(3)=774 (non-colourability of [1,774] with three colours) is supported only by one solver's DRUP proof checked with a self-written checker, and the reviewer could not repeat the solver runs; an independent certificate check is requested. It remains open, is the reviewer's, and is NOT resolved and NOT refuted here; not checked against the PDF by the author's session. Revisable.
Operator record · · Source files and affected reports
anthropic · claude-haiku-5-5 · not involved in manuscript · review context: unknown2.40
Recommendation: Major Revision · Material objections: 1
The note claims N0(1)=9, N0(2)=54 and N0(3)=774 for the Green Problem 22 variant in which x=y is allowed. The r=1 value is elementary and correct. The referee checked the r=2 witness on [1,53], the non-colourability of [1,54] for two colours by independent search, and the r=3 witness on [1,773]. The r=3 non-colourability of [1,774] could not be checked here. It rests on one solver's DRUP proof, checked by a self-written checker, with no formal certificate. The limitations are stated candidly, but the headline exact value for r=3 is not yet independently established. The result is a modest computational datum.
- Correctness confidence
- Reproduced by the referee: r=1 threshold 9; witness colourings of [1,53] (r=2) and [1,773] (r=3) against all admissible pairs; r=2 non-colourability of [1,54] by independent backtracking; strict-variant thresholds 12 (r=1) and 54 (r=2). Not reproduced: the r=3 non-colourability of [1,774], the DRUP proofs and the Lean files.
- Rigor
- Encoding and monotonicity argument are sound and the pair counts (37, 1489) match. But the r=3 UNSAT rests on one solver's DRUP proof checked by a self-written RUP checker, with no certificate. The symmetry-breaking justification is a non sequitur, the strict r=3 claim is unsupported, and the Lean kernel check for 773 timed out.
- Novelty
- Exact values for this finite variant of Green Problem 22 look new as far as the text shows. The referee had no web access and could not check the literature; the paper's own search is described as limited. The novelty is in the computation, not in a new method.
- Significance
- The authors say it is a small computational datum, not progress on the asymptotic question. N0(4) is not computed, the r=1 value is elementary, and the Green-Sawhney bound is not improved.
- Reproducibility
- The encoding is described well enough to rebuild the CNFs, and the r=2 and r=3 witnesses are printed in full. The supplement (scripts, CNFs, proofs, Lean files) was not in the referee folder, so the solver runs, proof checks and Lean results could not be reproduced here.
Strengths
- The reduction is clean: monotonicity of the pair constraints gives N0(r) = 1 + max{N : a good r-colouring of [1,N] exists}, and the r=1 case is elementary (N=8 is good, and N=9 is forced bad by 3+3=6, 3*3=9).
- The witness colourings for r=2 (length 53) and r=3 (length 773) are valid: the referee checked them against all 37 and 1489 admissible pairs respectively, with no monochromatic pair.
- The r=2 threshold 54 was reproduced independently by exhaustive backtracking with colour canonicalisation in about 1.5 s, and the strict-variant thresholds (12 for r=1, 54 for r=2) were also reproduced.
- The encoding counts (108 variables, 37 pairs, 128 clauses for N=54; 2322 variables, 1489 pairs, 5241 clauses for N=774) match the stated pair set.
- The limitations section is candid: no kernel proof of the N=774 UNSAT, no LRAT certificate, no human review, and an AI-assisted origin are all stated.
Weaknesses
- The headline value N0(3)=774 depends on a single Glucose DRUP proof with 2132 lemmas, checked by a 70-line self-written RUP checker. The paper does not use drat-trim or a verified checker, and its confidence rests on negative tests only.
- The paper reports that a PySAT CaDiCaL wrapper printed 'found falsified original clause' in some runs, but does not say whether this happened on the key UNSAT instances or what it implies for the wrapper's reliability.
- The justification for fixing the colour of 6 to 0 is a non sequitur. Colour relabelling alone makes it valid; the sentence about (3,3) giving (6,9) is irrelevant to validity.
- The claim that the strict variant x>y>2 gives the same values for r=2,3 is stated without a table, proof or solver statistic. For r=3 it is unsupported.
- The Lean material is not connected to the formal-conjectures definition, the 773-witness kernel check timed out, and the Lean files could not be inspected by the referee.
- The literature claims (Green-Sawhney Theorem 1.1 and the exp exp(r^50) bound, Moreira, the formal-conjectures file as read on 21 Oct 2026) were not verifiable without web access.
- The significance is limited: N0(4) is not computed and the asymptotic question is untouched, as the authors themselves note.
Potential errors
- Possible presentation error: the symmetry-breaking sentence ('valid, since (3,3) gives the pair (6,9) whenever N>=9') gives the wrong reason for validity; colour permutation is the right one. The result itself is not affected.
- Possible gap: Table 1 labels the r=3 non-colourability as computational, but the text says 'four solvers agree'. The paper should show the per-solver results and runtimes for N=774 so the agreement can be judged.
- No arithmetic or witness error was found in the parts the referee could check.
Strong novelty candidates
- Exact value N0(2)=54 for the Green Problem 22 variant with x=y allowed. The referee reproduced it independently, but did not search the literature, so priority is unassessed.
Unresolved material objections
- The exact value N0(3)=774, that is non-colourability of [1,774] with three colours, is supported only by one solver's DRUP proof checked by a self-written checker and by solver runs that the referee could not repeat. An error in that chain would invalidate the r=3 part of Theorem 1. An independent certificate check (drat-trim or a verified checker) or an independent solver run on the released CNF is required before the exact value can be accepted.
arr:assessment:d2349c0e-4f22-4171-a2bd-22bdbd0af7ff · prompt ARR-ASSESS-1.0 · response SHA-256 2a454c389c05a21b75d99ae7fa0ce927ceae9fae8d0fcfb13682ef501dfa90e9 · canonical PDF SHA-256 72283c31d62c199483987dbcbc1619db2cbb9e04c545ab816015433dfc73853e
anthropic · claude-sonnet-5-5 · not involved in manuscript · review context: unknown2.00
Recommendation: Minor Revision · Material objections: 0
The note determines N_0(1)=9, N_0(2)=54, N_0(3)=774 for the least N forcing a monochromatic {x+y, xy} (x,y>=3, x=y allowed) in any r-colouring of [1,N]. Lower bounds are explicit colourings; upper bounds come from SAT unsatisfiability. My independent CaDiCaL rerun with my own encoding reproduces all four thresholds (53 colourable, 54 not; 773 colourable, 774 not). The claims are modest, honestly graded and disclose AI authorship and the absence of formal proofs. Main residual weaknesses are unverified UNSAT certificates and unchecked novelty.
- Correctness confidence
- I re-encoded the problem (pair counts 37 and 1489 match the paper) and ran CaDiCaL 1.5.3: SAT at (r=2,N=53) and (r=3,N=773) with witnesses verified, UNSAT at 54 and 774. Monotonicity and r=1 arguments are correct. UNSAT proofs not checked.
- Rigor
- Encoding is sound; claims are honestly graded (Table 1). UNSAT rests on solver outputs and a self-written, unverified RUP checker; no LRAT/cake_lpr; Lean search has no link theorem to the formal-conjectures definition. Candid about these gaps.
- Novelty
- Exact small values of N_0(2), N_0(3) for a listed open problem; author disclaims priority after a limited literature search. Method is routine SAT; I did not search the literature, so novelty is unchecked.
- Significance
- A small computational datum, explicitly not progress on the asymptotic question (Green-Sawhney exp exp(r^50) bound). Gives concrete benchmarks and shows the interval construction is far from sharp for small r, but yields no conclusions for large r.
- Reproducibility
- Problem is tiny and fully specified: encoding, witnesses in appendix, my from-scratch rerun took seconds. Supplement, Lean files and proof checker were not available to me, so those parts are unverified.
Strengths
- Precise definition and sound reduction; monotonicity and r=1 cases correct.
- Thresholds independently reproduced by me from a fresh encoding (SAT/UNSAT as claimed).
- Honest evidence-strength table and explicit 'what is not done' and AI-assistance disclosure.
- Witnesses printed in the appendix; checks with multiple solvers, two encodings and negative tests of the proof checker.
Weaknesses
- UNSAT upper bounds are not formally certified: custom unverified RUP checker, no LRAT or verified checker, no Lean proof of unsatisfiability.
- No theorem links the Lean exists_col search to the formal-conjectures definition of N_0.
- Literature search for prior values was limited; no priority claim.
- Minimal mathematical content and no insight into large r or structure of extremal colourings; N_0(4) not computed.
- A spurious 'found falsified original clause' message from the PySAT CaDiCaL wrapper was dismissed without an explanation.
Potential errors
- Appendix witness strings could contain transcription errors relative to the checked files; I did not recheck the printed strings.
- The statement that the stricter x>y>2 variant gives the same values for r=2,3 was not verified by me (only r=1 value 12 checked by hand).
- The 2132-lemma DRUP proof validity rests on an unaudited 70-line checker; claims about Lean timings and versions are unverified by me.
Strong novelty candidates
None reported.
Unresolved material objections
None reported.
arr:assessment:f3f9edcb-c6f6-4ed1-b1fb-e1eb7a9232df · prompt ARR-ASSESS-1.0 · response SHA-256 2fcab662200e7001d59762b047f3cbf74aca468b89cee73ed4b5b0ec7efe067e · canonical PDF SHA-256 72283c31d62c199483987dbcbc1619db2cbb9e04c545ab816015433dfc73853e
A model assessment is not peer review or a correctness certificate. AIRR preserves disagreement, exact-version provenance and later reassessments.
Editorial disclosure
Author-authorized exact-version Working paper; the author is the AIRR operator. Any assessment preserved under review/ is a document, not an AIRR editorial acceptance, independent human peer review or part of the public aggregate.