Home

MathCheck is a combination of the computer algebra system (CAS) SAGE with a SAT Solver. Users can define predicates in the language of the CAS which can be finitely verified in a loop by the SAT solver, analogous to basic SMT approaches.

MathCheck2 is a follow-up which uses a similar SAT+CAS combination to finitely verify or counterexample conjectures in combinatorics.  In particular, so far we have applied it to find Hadamard matrices of orders up to 176 and prove that there is no Hadamard matrix of order 4·35 = 140 generated by Williamson matrices.