Overview

MathCheck is a system applying Boolean satisfiability (SAT) solvers and computer algebra systems (CASs) in order to efficiently search for mathematical objects and automatically generate computer-assisted proofs of mathematical conjectures.  MathCheck combines the efficient search and learning routines of SAT solvers with the efficient algorithms and expressiveness of CASs, thereby achieving the best of both worlds: MathCheck often solves problems thousands of times faster than either a SAT solver or a CAS.

The MathCheck project is led by professors Vijay Ganesh of Georgia Tech and Curtis Bright of the University of Windsor.  MathCheck was started in 2015 at the University of Waterloo by Vijay Ganesh, and it is now a multi-university project with members from the University of Windsor, Carleton UniversityWilfrid Laurier University, and the Georgia Institute of Technology.

Latest News

A survey article on MathCheck was published in the Communications of the ACM.

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

We are accepting applications for open research positions to work on MathCheck.

Successful applications

To date the MathCheck project has achieved the following successes:

In the process of performing these verifications, MathCheck has also explicitly constructed many new combinatorial objects:

Additionally, a component of the MathCheck project is designing programmatic SAT solvers, 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.