In this talk we de­scribe a com­bi­na­to­r­ial search method that com­bines the search power of Boolean sat­is­fi­a­bil­ity (SAT) solvers with the math­e­mat­i­cal ex­pres­sive­ness of com­puter al­ge­bra sys­tems (CAS). We dis­cuss our sys­tem Math­Check and how the SAT+CAS method has been used to de­rive the best known re­sults in a num­ber of prob­lems from graph the­ory, geom­e­try, com­bi­na­torics, and num­ber the­ory. Specif­i­cally, we de­scribe how Math­Check has been used in the Ruskey-Sav­age hy­per­cube con­jec­ture (1993), Lam's prob­lem from dis­crete geom­e­try (1800s), and briefly out­line Heule's re­sult in the Had­wiger-Nel­son plane-colour­ing prob­lem (1950).