Upcoming Talks

A classical theorem of Tierney characterizes abelian categories as those additive categories which satisfy a further purely nonadditive property known as Barr exactness. In this talk I will explain a version of this result in the setting of higher category theory: an infinity category is Barr exact and additive if and only if it arises as the connective half of a t-structure on some stable infinity category.

Mathematical formalization is the process of digitizing mathematical definitions and results using a "proof assistant", a computer program capable of checking logical statements against a set of inference rules and some basic axioms. In recent years, the community of mathematicians working on formalization has grown rapidly and has reached milestones that demonstrate the ability to formalize results at the frontier of knowledge. Proof assistants have applications to mathematical research, teaching, and communication.

Seminar webpage:  https://guests.mpim-bonn.mpg.de/bianchi/wiqi.html