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.

If you require accommodation for communication, please contact our Access Coordinator at simonsevents [at] berkeley.edu with as much advance notice as possible.