Description

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 search for counterexamples.

The SAT+CAS approach has been found to be 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 tractible, though relying on a SAT solver alone is often inefficient because the SAT solver is not able to exploit the known combinatorial relationships proven by 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.

The aim of the MathCheck project is to develop a system which combines the best of both of the SAT and CAS worlds to find counterexamples and finitely verify conjectures in mathematics.  To date the MathCheck project has achieved the following successes:

• • Finitely verified the Ruskey–Savage conjecture up to order 5 for the first time

  • Finitely verified the Norine conjecture up to order 6 for the first time

  • Found the counterexample 35 to the Williamson conjecture

  • Verified that 35 is the smallest counterexample of the Williamson conjecture for the first time

  • Enumerated all Williamson matrices in all orders divisible by 2 or 3 up to order 70 for the first time

  • Found thousands of new Williamson matrices in even orders and one previously undiscovered set of Williamson matrices in order 63

  • Enumerated all complex Golay pairs up to order 25

  • Verified the Craigen–Holzmann–Kharaghani conjecture that complex Golay pairs of order 23 do not exist

Both MathCheck and MathCheck2 are open source and released under the MIT licence.

<MathCheck description here>

* First, motivate why we need computational methods to finitely verify combinatorial mathematical conjectures (answer: traditional proof methods don't work well)

* Second, why SAT+CAS? Answer: SAT is great as a combinatorial search engine, while CAS is a storehouse of mathematical knowledge.