[Facets-of-complexity] Invitation to Monday Lecture & Colloquium - December 10th 2018

[Ita Brunke <i.brunke@inf.fu-berlin.de>]

You are cordially invited to our next Monday Lecture & Colloquium on December 10th at 14:15 h & 16:00 h at FU Berlin.

Location:

Room 005 - Ground Floor
Freie Universität Berlin
Takustr. 9
14195 Berlin

Time: Monday, December 10th - 14:15 h

Lecture: Marijn Heule (University of Texas, Austin)

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

Abstract:

Progress in satisfiability (SAT) solving has enabled answering long-standing open questions in mathematics completely automatically resulting in clever though potentially gigantic proofs. We illustrate the success of this approach by presenting the solution of the Boolean Pythagorean triples problem. We also produced and validated a proof of the solution, which has been called the ``largest math proof ever''. The enormous size of the proof is not important. In fact a shorter proof would have been preferable. However, the size shows that automated tools combined with super computing facilitate solving bigger problems. Moreover, the proof of 200 terabytes can now be validated using highly trustworthy systems, demonstrating that we can check the correctness of proofs no matter their size.

Coffee & Tea Break
Room 134

Time: Monday, December 10th - 16:00 h s.t.

Colloquium: Ander Lamaison (Freie Universität Berlin)

Title: Ramsey density of infinite paths

Abstract:

In a two-colouring of the edges of the complete graph on the natural numbers, what is the densest monochromatic infinite path that we can always find? We measure the density of a path by the upper asymptotic density of its vertex set. This question was first studied by Erdös and Galvin, who proved that the best density is between 2/3 and 8/9. In this talk we settle this question by proving that we can always find a monochromatic path of upper density at least (12+sqrt(8))/17=0.87226…, and constructing a two-colouring in which no denser path exists. This represents joint work with Jan Corsten, Louis DeBiasio and Richard Lang.