BEGIN:VCALENDAR
CALSCALE:GREGORIAN
PRODID:iCalendar-Ruby
VERSION:2.0
BEGIN:VEVENT
DESCRIPTION: Progress in satisfiability (SAT) solving has enabled answering
long-standing open questions in mathematics completely automatically resul
ting in clever though potentially gigantic proofs. We illustrate the succes
s of this approach by presenting the solution of the Boolean Pythagorean tr
iples problem. We also produced and validated a proof of the solution\, whi
ch has been called the ``largest math proof ever''. The enormous size of th
e proof is not important. In fact a shorter proof would have been preferabl
e. However\, the size shows that automated tools combined with super comput
ing facilitate solving bigger problems. Moreover\, the proof of 200 terabyt
es can now be validated using highly trustworthy systems\, demonstrating th
at we can check the correctness of proofs no matter their size.
DTSTAMP:20181127T164200
DTSTART:20181210T141500
CLASS:PUBLIC
LOCATION:Freie Universität Berlin \n Institut für Informatik \n Takustr. 9
\n 14195 Berlin \n Room 005 (Ground Floor)
SEQUENCE:0
SUMMARY:Marijn Heule (University of Texas\, Austin): Everything'\;s Big
ger in Texas: "\;The Largest Math Proof Ever"\;
UID:94644411@www.facetsofcomplexity.de
URL:http://www.facetsofcomplexity.de/monday/20181210-L-Heule.html
END:VEVENT
END:VCALENDAR