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&#x27\;s Big
 ger in Texas: &quot\;The Largest Math Proof Ever&quot\;
UID:94644411@/www.mi.fu-berlin.de
URL:https://www.mi.fu-berlin.de/en/facetsofcomplexity/monday/20181210-L-Heu
 le.html
END:VEVENT
END:VCALENDAR