Overview

MathCheck is a system which combines functionality from Boolean satisfiability (SAT) solvers and computer algebra systems (CAS) to verify and discover counterexamples to conjectures in mathematics.

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, though relying on these solvers alone is often not sufficient because they do not exploit combinatorial relationships known to mathematicians. On the other hand, CASs contain a storehouse of mathematical knowledge but typically lack the sophisticated combinatorial search engine of SAT solvers.  MathCheck combines the search power of a SAT solver with the mathematical power of a CAS.

Latest News: MathCheck awarded a €4,000 prize for the AAECC best paper in 2020.

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.

Citing

If you would like to cite MathCheck in your work, we suggest using the following BibTeX reference:

@inproceedings{bright2016mathcheck2,
  title={\textsc{MathCheck2}: A {SAT}+{CAS} Verifier for Combinatorial Conjectures},
  author = {Curtis Bright and Vijay Ganesh and Albert Heinle and Ilias Kotsireas and Saeed Nejati and Krzysztof Czarnecki},
  booktitle = {Computer Algebra in Scientific Computing}
  pages = {117--133},
  year = {2016},
  publisher = {Springer International Publishing},
  doi = {10.1007/978-3-319-45641-6_9},
  url = {https://doi.org/10.1007/978-3-319-45641-6_9}
}

Also see our publications page for more recent applications of MathCheck.