Elif Uskuplu, USC

Abstract: In this talk, we will discuss proof assistants and their practical applications. We will introduce what it means to use a proof assistant. Afterward, we will talk about Lean mathlib, which is currently the largest formalized mathematics library, and Agda unimath, which is an ongoing project that I also contribute to. We will not assume any prior knowledge, and the talk is open to everyone.