For problem #273 (is there a covering system of ℤ, all of whose moduli are of the form p-1 for primes p≥5?), a computational partial result:
There is no covering system with pairwise distinct moduli all of the form p-1 ≤ 50 (p prime ≥ 5).
Method: the full pool of admissible moduli up to 50 is {4, 6, 10, 12, 16, 18, 22, 28, 30, 36, 40, 42, 46} (13 moduli, lcm L = 1,275,120). A covering system with moduli restricted to this pool exists iff a Boolean formula is satisfiable: one variable per congruence class (n, a), pairwise at-most-one per modulus (enforcing distinct moduli), and one clause per residue mod L (coverage). CaDiCaL 3.0.0 reports this CNF (310 variables, 1,279,875 clauses) UNSAT.
The result doesn't rest on trusting the solver: the LRAT unsatisfiability certificate was checked by three independent checkers, including cake_lpr, the formally verified (HOL4/CakeML) LRAT checker used for SAT Competition proof certification.
Obvious limitation: this only rules out moduli ≤ 50; the general problem stays open. The next admissible modulus is 52 (=4·13), which multiplies L by 13 — the direct-encoding approach hits diminishing returns quickly after this, so further progress here likely needs a structural argument rather than a bigger computation.
Code (deterministic CNF generator + verification instructions) and the certificate: https://github.com/Sanexxxx777/erdos-computational-bounds/tree/main/sat273
For problem #273 (is there a covering system of ℤ, all of whose moduli are of the form p-1 for primes p≥5?), a computational partial result:
There is no covering system with pairwise distinct moduli all of the form p-1 ≤ 50 (p prime ≥ 5).
Method: the full pool of admissible moduli up to 50 is {4, 6, 10, 12, 16, 18, 22, 28, 30, 36, 40, 42, 46} (13 moduli, lcm L = 1,275,120). A covering system with moduli restricted to this pool exists iff a Boolean formula is satisfiable: one variable per congruence class (n, a), pairwise at-most-one per modulus (enforcing distinct moduli), and one clause per residue mod L (coverage). CaDiCaL 3.0.0 reports this CNF (310 variables, 1,279,875 clauses) UNSAT.
The result doesn't rest on trusting the solver: the LRAT unsatisfiability certificate was checked by three independent checkers, including
cake_lpr, the formally verified (HOL4/CakeML) LRAT checker used for SAT Competition proof certification.Obvious limitation: this only rules out moduli ≤ 50; the general problem stays open. The next admissible modulus is 52 (=4·13), which multiplies L by 13 — the direct-encoding approach hits diminishing returns quickly after this, so further progress here likely needs a structural argument rather than a bigger computation.
Code (deterministic CNF generator + verification instructions) and the certificate: https://github.com/Sanexxxx777/erdos-computational-bounds/tree/main/sat273