Informalizing formalized mathematics using the Lean theorem prover
Friday, 21.4.23, 10:30-11:30, Hörsaal II, Albertstr. 23b
One of the applications of interactive theorem provers in\npure mathematics is being able to produce machine-verified formal proofs. I will talk about a less-obvious application, which is using formalized mathematics to author interactive informal expositions. I will demonstrate a prototype of an "auto-informalization" system written in Lean that presents the reader with an interface to view proofs at a desired level of detail. I will also discuss thoughts on the impact of such tools in mathematics. This is joint work with Patrick Massot.\n
Syzygies of the cotangent complex
Friday, 28.4.23, 10:30-11:30, Hörsaal II, Albertstr. 23b
The cotangent complex is an important but difficult to understand object associated to a map of commutative rings (or schemes). It is connected with some easier to compute invariants: the module of differential forms, the conormal module, and Koszul homology can all be seen as syzygies inside the cotangent complex. Quillen conjectured that, for maps of finite flat dimension, the cotangent complex can only be bounded for locally complete intersection homomorphisms. This was proven by Avramov in 1999. I will explain how to get a new proof by paying attention to these syzygies, and how to simultaneously prove a conjecture of Vasconcelos on the conormal module.
Combinatorics of toric bundles
Friday, 28.4.23, 14:00-15:00, SR 119
Toric bundles are fibre bundles which have a toric variety as a fiber. One particularly studied class of toric bundles are horospherical varieties which are toric bundles over generalized flag varieties. Similar to toric varieties, toric bundles admit a combinatorial description via polyhedral geometry. In my talk, I will explain such a combinatorial description, and describe a couple of results which rely on it. In particular, I will present a generalization of the BKK theorem and the Fano criterion for toric bundles.