Abstract
Mathematical intuition is often sparked by examples and counterexamples. The bad news? Constructing good examples can be difficult. The good news? SAT solvers and automated reasoning tools can help. In this talk, I will demonstrate how SAT solvers can generate insightful constructions in discrete mathematics, leading to new conjectures and concrete results. Through a series of case studies, we will see how computational search can challenge intuition, suggest patterns, and even guide mathematical discovery.