Abstract
Automated reasoning has become increasingly powerful and popular. This enabled solving very hard problems ranging from determining the correctness of complex systems to answering long-standing open questions in mathematics. Moreover, we can have full confidence in the correctness of the solutions by producing certificates (proofs of unsatisfiability) that can be validated using trustworthy systems.
The talk covers some successes, including the solutions with proofs of the Boolean Pythagorean Triples problem, Keller's conjecture, and the packing chromatic number of the infinite square grid. The proofs are gigantic, but they have been validated using a formally-verified proof checker. These results underscore the effectiveness of automated reasoning to solve hard challenges arising in mathematics and elsewhere, while having stronger guarantees of correctness than pen-and-paper proofs.