Trustworthy and Distributed Automated Reasoning | Richard M. Karp Distinguished Lecture

We're delighted to share this Richard M. Karp Distinguished Lecture by Marijn Heule (Carnegie Mellon University), given on March 19, 2021.

Abstract: Automated reasoning has become increasingly powerful over the past decades thanks to algorithmic breakthroughs and expanding processing capabilities. This made possible and popularized its usage in solving very hard problems ranging from determining the correctness of complex systems to tackling long-standing open problems in mathematics. This talk presents an overview of progress in trustworthy and distributed automated reasoning and covers some of its successes, including the solutions — with proofs — of the Boolean Pythagorean triples problem and Keller's conjecture. Although some proofs are gigantic, they can be (and have been) independently validated using efficient, formally verified proof checkers. These results underscore the effectiveness of automated reasoning to solve hard challenges in mathematics and elsewhere, while obtaining stronger guarantees of correctness than pen-and-paper proofs.