I’ve been building a CDCL SAT solver from scratch for the past year, and it just produced something I think is worth sharing: a machine-verified proof that R(5,5) ≤ 43. R(5,5) is the smallest n such that every 2-coloring of the edges of the complete graph Kₙ contains a monochromatic K₅. The upper bound R(5,5) ≤ 43 has been known since Exoo (1989) but to my knowledge has never had a complete machine-verified proof published. The proof is structured as three independently machine-verified components: • Proof A — Each of 1722 lex symmetry-breaking clauses added to the bare K₄₃ CNF is SR-redundant, verified by VeriPB via dom/deld steps • Proof B — The augmented CNF (bare + 1722 axioms) is UNSAT, verified by VeriPB • Proof S — The Satsuma symmetry-augmented CNF is equisatisfiable with the bare CNF, verified by VeriPB The composition step — “adding SR-redundant clauses preserves equisatisfiability” — is not informal. It’s the central result of Heule, Kiesl, Biere “Short Proofs Without New Variables” (CADE-26, 2017, Best Paper Award), the same theorem underlying drat-trim’s soundness. It’s implicit in every DRAT-verified proof in the literature; here it’s explicit and cited. Everything is publicly available and independently verifiable: Repo: https://github.com/lioncash3k6-ux/Ramsey-5-5-43-solution Release (67MB proof package): https://github.com/lioncash3k6-ux/Ramsey-5-5-43-solution/releases/tag/v1.0 MD5: 97f2ee66dc1318fcff07e644c3eb7927 Clone the repo, download the release, run verify.sh. Every step is checkable. I’m a self-taught developer, not an academic. I’d genuinely welcome scrutiny from anyone who knows this area — especially on the composition argument or the SR witnesses in Proof A. If there’s a gap, I want to know. submitted by /u/Xeophrix
Originally posted by u/Xeophrix on r/ArtificialInteligence