Everything's Bigger in Texas: ``The Largest Math Proof Ever''

Add to your list(s) Download to your calendar using vCal

• Marijn Heule (University of Texas at Austin)
• Wednesday 12 July 2017, 16:00-17:00
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

This talk has been canceled/deleted

Co-authors: Oliver Kullmann (Swansea University) and Victor Marek (University of Kentucky)Many search problems, from artificial intelligence to combinatorics, explore large search spaces to determine the presence or absence of a certain object. These problems are hard due to combinatorial explosion, and have traditionally been called infeasible. The brute-force method, which at least implicitly explores all possibilities, is a general approach to search systematically through such spaces. Brute force has long been regarded as suitable only for simple problems. This has changed in the last two decades, due to the progress in satisfiability (SAT) solving, which renders brute force into a powerful approach to deal with many problems easily and automatically.We illustrate the strength of SAT via the Boolean Pythagorean Triples problem, which has been a long-standing open problem in Ramsey Theory. Our parallel SAT solver allowed us to solve the problem on a cluster in about two days using 800cores, demonstrating its linear time speedup on many hard problems. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proof checking, we produced and verified a clausal proof of the smallest counterexample, which is almost 200 terabytes in size. These techniques show great promise for attacking a variety of challenging problems arising in mathematics and computer science.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.