4th of November, 2021. Part of the Topos Institute Colloquium.
-----
Abstract: Modern logic tells us that mathematics can be formalized, in principle. Computational proof assistants, developed over the last half century, make it possible to do so in practice. In this talk, I will briefly survey the state of the field today and discuss some of the reasons that formalization is desirable. I will discuss one particular proof assistant, Lean, and its library, mathlib. I will explain why dependent type theory, Lean's underlying logical framework, provides an attractive platform for formalization. Finally, I will consider ways that formal mathematics can support and enhance the Topos Institute's missions.
Негізгі бет Ғылым және технология Jeremy Avigad: "Formal mathematics, dependent type theory, and the Topos Institute"
Пікірлер: 7