In this talk we describe a combinatorial search method that combines the search power of Boolean satisfiability (SAT) solvers with the mathematical expressiveness of computer algebra systems (CAS). We discuss our system MathCheck and how the SAT+CAS method has been used to derive the best known results in a number of problems from graph theory, geometry, combinatorics, and number theory. Specifically, we describe how MathCheck has been used in the Ruskey-Savage hypercube conjecture (1993), Lam's problem from discrete geometry (1800s), and briefly outline Heule's result in the Hadwiger-Nelson plane-colouring problem (1950).