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.