Lam's problem is to prove the nonexistence of a type of geometric structure that has intrigued mathematicians for centuries. In this work we reduce Lam's problem to a Boolean satisfiability (SAT) problem and generate certificates which for the first time can be used to verify the resolution of Lam's problem. The search space underlying the problem has many nontrivial symmetries⁠—necessitating an approach that detects and removes symmetries as early as possible. We couple a method of isomorph-free exhaustive generation with a SAT solver and show that this significantly improves the performance of the solver when symmetries are present.