MathCheck is a system using Boolean satisfiability (SAT) solvers coupled with computer algebra systems (CASs) in order to efficiently search for mathematical objects and provide computer-assisted proofs of mathematical conjectures.  MathCheck combines the efficient search and learning routines of SAT solvers with the efficient mathematical algorithms of CASs, thereby achieving the best of both worlds.

MathCheck was initiated at the University of Waterloo and is now a multi-university project with members from the University of Windsor, Carleton University, and Wilfrid Laurier University.

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

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

List of successful applications

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 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.


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

  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.