MathCheck is a system which combines functionality from Boolean satisfiability (SAT) solvers and computer algebra systems (CAS) to verify conjectures in mathematics up to a finite bound and to search for counterexamples.
The SAT+CAS approach is particularly effective for combinatorial conjectures, as many conjectures in combinatorics reduce to a huge combinatorial search for which there are no known efficient algorithms. Using a SAT solver can make such searches tractable for many combinatorial conjectures, though relying on these solvers alone is not sufficient because they are not able to exploit combinatorial relationships known to mathematicians. On the other hand, computer algebra systems contain a storehouse of mathematical knowledge but typically lack the sophisticated combinatorial search engine of SAT solvers.
List of mathematical conjectures resolved
The aim of the MathCheck project is to develop a SAT+CAS system which combines the best of both worlds and can find counterexamples or finitely verify conjectures in mathematics. To date the MathCheck project has achieved the following successes:
- Verified that 35 is the smallest counterexample of the Williamson conjecture for the first time
- Verified the even Williamson conjecture up to order 70 for the first time
- Verified all the Craigen–Holzmann–Kharaghani conjectures about complex Golay pairs up to length 28 (e.g., complex Golay pairs of lengths 23 and 28 do not exist)
- Found three new counterexamples to the conjecture that good matrices exist in all odd orders
- Verified the best matrix conjecture up to order 57 for the first time
- Verified the Ruskey–Savage conjecture up to order five for the first time
- Verified the Norine conjecture up to order six for the first time
- Verified the weight 15 case of Lam's problem and produced a nonexistence certificate for the first time
In the process of performing these verifications MathCheck has also explicitly constructed a number of combinatorial objects:
- Enumerated all Williamson matrices in even orders up to order 70 for the first time (finding over 100,000 new Williamson matrices and resulting in the first proof that Williamson matrices exist in all orders of the form 2k)
- Found one previously undiscovered set of Williamson matrices in order 63
- Found eight-Williamson matrices in all odd orders up to and including 35 for the first time
- Found all complex Golay pairs up to length 28 with publicly available results for the first time
- Found a new set of good matrices in order 57 and a set of good matrices in order 27 that was missed by all previous searches
- Found three new sets of best matrices in order 57 (the largest best matrices currently known)
- Found a new partial projective plane with 111 rows and 51 columns previously claimed to not exist
Additionally, a component of the MathCheck project is designing custom-tailored SAT solvers using the programmatic SAT paradigm, currently specializing in combinatorial matrix problems defined via periodic and aperiodic correlation. Both MathCheck and MathCheck2 are open source and released under the MIT licence.
