Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems with precise grammars and rules of use. Building on such foundations, computational proof assistants now make it possible to encode mathematical knowledge in digital form. In this talk, I'll explore some of the ways that these and related technologies can help us do mathematics.

Jeremy Avigad is a professor of philosophy and a professor of mathematical sciences at Carnegie Mellon University. He received a B.A. in mathematics from Harvard University in 1989, and a Ph.D. in mathematics from the University of California at Berkeley in 1995 under the supervision of Jack Silver. He has contributed to the areas of mathematical logic and foundations, formal verification and interactive theorem proving, and the philosophy and history of mathematics. He became Director of the Hoskinson Center for Formal Mathematics at Carnegie Mellon University after Charles Hoskinson donated $20 Million in September 2021 to establish it.

For some insightful discussions afterwards, and to meet with the speaker, we invite you to join us over dinner in downtown Karlsruhe right after the talk. If you would like to join in for dinner, please register by sending an email to mathsee ∂does-not-exist.kit edu (no registration needed for attending the talk).

The talk & the dinner are aimed at a broad scientific audience and everyone is welcome to attend!

Download Link: Event Poster