Certified Ramsey Number Bounds on Commodity 8-Core Hardware: Two-Sided Independent Certification (DRAT + cost=0 Witnesses)

A SAT solver can hand you a wrong answer and look completely confident doing it. That is the problem this package is built around. So the rule here is simple and it never bends: nothing counts unless a second tool, one that had no part in producing the result, confirms it. Every upper bound is a DRAT proof, and drat-trim rechecks it reading only the formula and the proof, so a buggy solver cannot sneak a bad proof past it. Every lower bound is an explicit graph coloring, and separate clique-counting code confirms it has no monochromatic clique. Two witnesses for every claim, from two tools that do not trust each other. What you get, all reproducible from the files in this deposit: Four Ramsey numbers settled exactly. R(3,3)=6, R(3,4)=9, R(3,5)=14, R(4,4)=18. Each one has a DRAT proof that drat-trim confirmed (4 of 4 reported "s VERIFIED" in this session) on the upper side, and a cost=0 witness on the lower side. These are known values; the contribution is the certified, two-sided pipeline that produces them without a human in the loop. 87 lower bounds with cost=0 witnesses, across 15 fronts from R(3,6) up to R(7,7). That includes the open numbers: R(5,5) > 35, R(6,6) > 52, R(5,6) > 45, R(5,7) > 45. Here is the honest part, stated up front so nobody has to dig for it: for the open numbers these bounds sit far below the best constructions in the literature. This was run on a commodity 8-core machine, and beating the record was never the point. The point is that every one of those 87 bounds carries an independently rechecked witness. R(3,5)=14, confirmed two ways. Once by direct SAT (the DRAT proof plus drat-trim), and once by a completely separate method, one-vertex extension over the critical layer. At n=13 the generator enumerated the full critical layer (exactly one non-isomorphic graph), the minimum of the extension count over that complete layer is positive, so R(3,5) is at most 14. Two methods that share no code landing on the same number is the strongest confirmation in the package. An audit of Machura's claimed R(5,5)=43 proof. We reimplemented the Shadow Formula method from scratch, and on every case where the critical layer can be fully enumerated it gives the right answer: R(3,3), R(3,4), R(3,5) all check out. The method is correct. The R(5,5)=43 claim is a different matter. It needs the extension count taken as a minimum over the entire critical layer of K42 graphs, and a minimum over an incomplete set can only sit at or above the true minimum, never below it. Machura tested 674 graphs that his own files describe as not a complete catalogue ("Completeness is not claimed", in his words). So the value he reports is an upper estimate on the real quantity, and it does not rule out a missed graph that would collapse the argument. This is a gap in the argument, not an error in the method. R(5,5) stays open in the range [43, 46]. The same discipline applies to our own work. The R(4,4) extension result leans on a literature fact (that Paley(17) is the only critical graph at that size), and we flag that openly rather than passing it off as something we verified ourselves, because that is exactly the gap we just faulted in someone else. The R(4,4)=18 upper bound from the SAT side does not need that assumption and stands on its own. What this hardware cannot do is also written down plainly. Upper bounds past R(4,4)=18 did not finish under any method tried, including multi-hour single-solver runs and cube-and-conquer; that proof exists but it needs a cluster. The lower-bound search hits two walls, a per-instance solve timeout and an encoding blowup where the clause count runs into the tens of millions. None of that is hidden. Everything needed to rerun it is included: the four DRAT proofs and their CNFs, all 91 witness files, the Rust extension kernel, the dual-method scripts, the full Machura audit, a reproduction log, and SHA-256 checksums for every file. A stranger with this download and the standard tools (CaDiCaL, drat-trim, nauty geng, Python 3.12, a Rust toolchain) can verify the lot. This is a new version of an earlier R(5,5)-only record (concept DOI 10.5281/zenodo.20431368), widened from that single analysis into the full certification toolkit. Authors: Paulina Janowska; Gniewislawa AI / Hermes (autonomous research agent). gniewka.antydizajn.plLicense: CC-BY-4.0