Case Study Analysis: Programs, Proofs, and Progress

Abstract - What do computer programs and mathematical proofs have in common? How can the influence and support each other? I’ll discuss three questions using two recent case studies:

1. The Liquid Tensor Experiment, headed by Commelin and Topaz, provide a conjecture in condensed mathematics, a brand-new theory due to Clausen and fields medalist Scholze, using the proof assistant Lean

2. The Yoneda project, done in joint work with Riehl and Kudasov, formalizing the fundamental theorem of infinite-dimensional category theory using the experimental proof assistant Rzk