Dihedral and cyclic Ramsey numbers of the alternating 3-path
for all — the slice of Conjecture 4.9 (Damnjanović–Đorđević, arXiv:2607.06817) and Conjecture 4.23 (Bašić–Damnjanović–Stevanović–Stošić, arXiv:2604.16188).
- Result
- Proved(see note)
- Status
- Resolved
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Permutational Ramsey theory
- Posed by
- Damnjanović–Đorđević (Conj 4.9); Bašić–Damnjanović–Stevanović–Stošić (Conj 4.23)
- Year posed
- 2026
- Years open
- 0y
- Solved
- 2026-08-12
- Model
- Claude Fable
- Vendor
- Anthropic
- Collaborators
- —
- Verification
- Site-confirmed
- Publication
- Preprint
- Significance
- 5 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
The a = 3 slice is settled outright; the parent conjectures, asserting 1 + (a-1)(b-1) for all a, remain open for every a >= 4, where the upper bound is the hard part.
What the AI did
The model produced the proof (the collapse, the Chvátal reduction, the cyclic corollary), the Lean 4 formalization, and the Python verification script autonomously. Human direction was limited to initiation and operational supervision.
Verification
Reproduced by this site on 13 August 2026. The Lean development builds clean (exit 0) with the pinned toolchain (lean4 v4.12.0, core only, no Mathlib). Its own #print axioms output shows all five main theorems — theoremB_lowerBound, theoremB_lowerBound_all_groups, lemma2_blockWitness, lemma3_dih3_eq_sym3, noMonoCopy_completeGraph_reduce — depending on exactly propext, Classical.choice and Quot.sound. No Lean.ofReduceBool, so no native_decide behind the result; with comments stripped the source has zero sorry, admit, axiom declarations and native_decide, and its 23 decide calls are kernel-reduced. A naive grep contradicts this only because those words appear in the file's own documentation. The Python checker runs as described: Dih(3) has order 6 and equals Sym(3) (against Dih(4) at 8 of 24), lower-bound witnesses are valid for b = 2..8, and b = 3 is settled exhaustively over all 1,024 colourings of K5. The upper bound for general b is not formalized; it cites Chvatal 1977, R(T, K_n) = (|T|-1)(n-1)+1, giving 2b-1 for the three-vertex path — standard, and the arithmetic checks out. Two things unconfirmed: the claimed DRAT-certified SAT recomputation for b = 2..7 has no CNF, certificate or solver log in the ten-file repository; and there is no human peer review, this being a self-submission of AI-produced work reviewed by AI agents inside the producing pipeline.
Sources
- Lean proofGitHub repo (preprint + Lean proof + Python checker)
- CodeEvidence repository: preprint, Lean proof, Python checker
- Problem recordDamnjanovic and Djordjevic, Computation of small reflective and dihedral Ramsey numbers (Conjecture 4.9)Basic, Damnjanovic, Stevanovic and Stosic (Conjecture 4.23)
Submitted by ZestyWombat854 on