A negative computational result looks compact after the work is finished: no example exists below a stated bound. Earning that sentence responsibly requires much more than running a solver. Every case must be covered, every timeout kept separate from an impossibility result, and every remaining reason for doubt made visible.
The project takes the form of a public collection of exact-cover, CP-SAT, and SAT solvers, exhaustive run records, and an audit program for the three-hit IRDCS existence problem. Its purpose is to narrow an open combinatorics problem with an inspectable exhaustive search while keeping the difference between computational evidence and proof visible.
The question behind Three-Hit IRDCS Search
An incongruent restricted disjoint covering system partitions an interval using congruence classes with distinct moduli. In the three-hit version, every selected class must contain at least three points of the interval. The existence question appears in a 2009 paper and later resurfaced in a MathOverflow collection of open problems suited to computational experimentation. Researchers in computational combinatorics, exact cover, and AI-assisted mathematics can inspect or extend the work. Anyone citing the lower bound is affected by its verification quality, so the preliminary status and missing independent replication must remain prominent.
How Three-Hit IRDCS Search took shape
The search translates each candidate congruence class into a row of an exact-cover instance. A C++ Algorithm X solver with dancing links covers interval points exactly once while treating modulus use as an at-most-once constraint. A structural minimal-counterexample argument reduces the least modulus to at least four; the hardest interval lengths are then partitioned by their exact least selected modulus, and a separate audit checks that every required branch has a recorded exhaustive UNSAT result. Josiah asked an OpenAI Codex agent to attempt another unsolved problem, directed the standards for verification, attribution, and publication, and accepted responsibility for the public artifact. Codex selected this problem within that scope, formulated and implemented the searches, ran the recorded computations, interpreted the output, and drafted the documentation.
Method diagram · exhaustive-search boundary
A lower-bound claim is assembled from complete, auditable branches.
Preliminary computational lower bound: n≥108 if a three-hit IRDCS exists · not a theorem
What the evidence supports
The repository records exhaustive UNSAT coverage for whole instances from n=4 through n=101 and complete least-modulus branch partitions from n=102 through n=107. The included audit passes over those records, and rebuilt dancing-links and independent CP-SAT formulations agree on the smaller n=60 control instance. The current contribution is a narrowed search frontier and a reproducible research object, not closure of the mathematical problem. It is also a useful test of agent-led research: the artifact is credible to the extent that another person can inspect the assumptions, rerun the code, challenge the reduction, and eventually replace trust in the original computation with independent evidence.
The large UNSAT runs do not produce independently checkable proof traces, no independent mathematician has replicated the full result, and agreement on smaller instances cannot establish that the large computation is bug-free. No three-hit construction was found, so existence remains open and n≥108 is a preliminary computational lower bound rather than a theorem. The most valuable next steps are an independent replication, expert review of the structural reduction, and a proof-producing SAT or comparable formulation that can emit a separately checkable certificate for the large UNSAT claims.