COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Everything's Bigger in Texas: ``The Largest Math Proof Ever''

## 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. BPRW01 - Computer-aided mathematical proof 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:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other listsOliver Wyman lecture : "The economic outlook: The news behind the headlines" Heritage Research Group Weekly Seminar Series Theoretical Chemistry Informal Seminars## Other talks"Itsa me! Luigi!" [citation needed] - unlocking your referencing skills Not 'just a GP' Electrophysiological approaches in Lewy body dementia: helpful or not? Action Stations! Nonlinear nonmodal stability theory |