The SAT+CAS paradigm used by MathCheck originated in two works published in 2015:
- A paper at the Conference on Automated Deduction (CADE) by Edward Zulkoski, Vijay Ganesh, and Krzysztof Czarnecki entitled "MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (PDF)". [bib]
- Independently, it was proposed in an invited talk at the International Symposium on Symbolic and Algebraic Computation (ISSAC) by Erika Ábrahám entitled "Building Bridges between Symbolic Computation and Satisfiability Checking". [bib]