You are cordially invited to our next Monday Lecture &
Colloquium on December 10th at 14:15 h & 16:00 h at FU Berlin.
Location: 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" Progress in satisfiability (SAT) solving has enabled answering
longstanding 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 In a
twocolouring 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
twocolouring in which no denser path exists. This represents
joint work with Jan Corsten, Louis DeBiasio and Richard Lang.
