14th edition: Charmey January 13 17, 2025
Tentative Schedule
Monday January 13 
Tuesday January 14 
Wednesday January 15 
Thursday January 16 
Friday January 17 

breakfast 
8:459:45 minicourse 
8:459:45 minicourse 
8:459:45 minicourse 
8:459:45 minicourse 
10:1511:15 minicourse 
10:1511:15 minicourse 
10:1511:15 minicourse 
10:0011:00 minicourse 
12:30 welcome 
11:4512:45 minicourse 
11:4512:45 minicourse 
11:4512:45 minicourse 
11:1512:15 minicourse 
lunch 
bus at 12:40 
14:3015:30 minicourse 
time for discussion / enjoying the mountain side 

16:0017:00 minicourse 
17:2018:10 talk 
17:2018:20 talk 
17:2018:10 talk 
17:3018:30 minicourse 
18:3019:20 talk 
18:3019:20 talk 
18:3019:20 talk 
19h dinner 
19:30 dinner 
Minicourses

Formalising arithmetic and geometry in Lean: an introduction
David Loeffler (UniDistance Suisse)
Abstract
This minicourse is an introduction to the Lean Theorem Prover, a computer program for formally checking the validity of mathematical proofs. The course will mostly focus on how to use the software in practice (rather than going too deep into the logical foundations). In particular, we'll see a tour of some of the theorems in number theory and algebraic geometry that have already been formalised in the huge "Mathlib" library, and try out formalising a few more lemmas for ourselves.
There will be lots of examples and exercises to try out, so you should bring a computer of your own that you can install Lean on. The software runs fine on Windows, Mac, and most Linux distributions (but is unlikely to work well on phones or tablets). Installing Lean on your computer yourself before arriving in Charmey is not obligatory, but might be a good idea if you want to get the most out of the course; see docs.leanlang.org/lean4/doc/quickstart.html for instructions.

Derived categories of coherent sheaves
Evgeny Shinder (University of Sheffield)
Abstract
We will start with a review of standard homological algebra, such as injective and projective resolutions and Extgroups. Then we discuss derived functors, mostly focussing on coherent sheaves, and in particular review the coherent sheaf cohomology. Finally we go into the construction of the derived category of coherent sheaves and study its properties.

Different cones of divisors: from Mori Dream Spaces to Ktrivial varieties
Zhixin Xie (Université de Lorraine)
Abstract
Given a variety, we consider the real vector space spanned by Cartier divisors modulo numerical equivalence. From the point of view of birational geometry, we are interested in the shape of the nef cone and the movable cone in this vector space.
For a Fano variety, i.e. a variety with ample anticanonical class, it follows from the Mori’s cone theorem that the nef cone is rational polyhedral. More generally for a Mori Dream Space, both the nef cone and the movable cone are rational polyhedral. However, these cones can be very wild in general: when we turn to Ktrivial varieties, i.e. varieties with numerically trivial canonical class, they behave less well than Fano varieties. For instance, we can construct examples of Ktrivial varieties for which the nef or the movable cone is round. Nevertheless, the KawamataMorrison cone conjecture predicts that the nef and the movable cones on a Ktrivial variety are rational polyhedral up to the action of natural groups acting on them.
In this course, we will introduce basic notions and techniques related to the description of different cones of divisors and we will illustrate them on many examples. In particular, we present tools from the Minimal Model Program and their application to connect different cones. We will introduce the KawamataMorrison conjecture and explain some known results. We will also discuss the cones of divisors of varieties with nef anticanonical class, which interpolate between Fano varieties and Ktrivial varieties.
Talks
Participants
Organizers
Andrea Fanelli (Bordeaux)
Philipp Habegger (Basel)
Julia Schneider (Sheffield)
Logistic support: Adrien Dubouloz (Poitiers)
Support
ANR Fracasso
Swiss Mathematical Society
Swiss Academy of Sciences
University of Basel