Overview

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:

In the process of performing these verifications MathCheck has also explicitly constructed a number of combinatorial objects:

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.