Speaker
Dagur Asgeirsson, University of Alberta
Abstract
Mathlib is a large, unified library of formalized mathematics written in Lean. One of its goals is to provide the necessary background material to be able to formally state the main definitions and results in modern research papers. In some areas of mathematics this is already possible, but in most there is still work to be done. The theory of ∞-categories is one big obstacle on the way to this goal. There are various ways to formalize it, each with its own merits and drawbacks. In this talk we discuss the feasibility of each of these approaches for mathlib and why we should formalize ∞-categories in mathlib.
Dagur Asgeirsson, University of Alberta
Abstract
Mathlib is a large, unified library of formalized mathematics written in Lean. One of its goals is to provide the necessary background material to be able to formally state the main definitions and results in modern research papers. In some areas of mathematics this is already possible, but in most there is still work to be done. The theory of ∞-categories is one big obstacle on the way to this goal. There are various ways to formalize it, each with its own merits and drawbacks. In this talk we discuss the feasibility of each of these approaches for mathlib and why we should formalize ∞-categories in mathlib.