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 was started at the University of Waterloo and run by Vijay Ganesh (now at Georgia Tech), and Curtis Bright has been the lead developer since 2016. MathCheck is now a multi-university project with members from the University of Windsor, Carleton University, Wilfrid 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:
- Verified Lam's problem and produced the first set of nonexistence certificates
- Verified that 35 is the smallest counterexample of the Williamson conjecture for the first time
- Derived a new lower bound on the size of the smallest Kochen–Specker system
- Verified the even Williamson conjecture up to order 70 and found the first examples of Williamson matrices of order 70
- First independent verification of the Craigen–Holzmann–Kharaghani conjectures about complex Golay pairs up to length 28
- Found three new counterexamples to the conjecture that good matrices exist in all odd orders
- Verified the best matrix conjecture up to order 57 for the first time
- Verified the Ruskey–Savage conjecture up to order five for the first time
- Verified the Norine conjecture up to order six for the first time
- First independent verification of the nonexistence of ovals in a projective plane of order ten
In the process of performing these verifications, MathCheck has also explicitly constructed many new combinatorial objects:
- Enumerated all Williamson matrices in even orders up to order 70 for the first time (finding over 100,000 new Williamson matrices—resulting in the first proof that Williamson matrices exist in all orders of the form 2k)
- Found a previously undiscovered set of Williamson matrices in order 63
- Found eight-Williamson matrices in all odd orders up to and including 35 for the first time
- Found all complex Golay pairs up to length 28 with publicly available results for the first time
- Found a new set of good matrices in order 57 and a set of good matrices in order 27 that was missed by all previous searches
- Found three new sets of best matrices in order 57 (the largest best matrices currently known)
- Found a new partial projective plane with 111 rows and 51 columns previously claimed to not exist
- Found four new Kochen–Specker candidates missed in the previous search
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.
