Note: tea is the talk (3:30 outside the main office in Altgeld) rather than after.
Title: Proofs and Conversations
Abstract: Proof assistants make it possible to write machine-checkable proofs about programs or about mathematics with the help of a computer. Once confined to the fringes of mathematics, their use is growing in popularity. This talk will discuss the connections between writing machine-checkable proofs and software engineering, and how we can use this connection to empower collaboration at a scale never before seen in mathematics.
