The GRACE Spring School brings together doctoral candidates and invited researchers for a week of lectures, tutorials, and informal discussions on the themes at the heart of GRACE: Geometry, Representations and Algebra through Computation and Experiments. The school is part of the activities of the GRACE Doctoral Training Unit at the University of Luxembourg, funded by the FNR.
The programme combines short research talks given by GRACE doctoral candidates with longer lectures by invited speakers, a hands-on tutorial on interactive theorem proving in Lean, and a half-day excursion. It takes place in the small town of Clervaux, in the north of Luxembourg, whose castle and surrounding forests provide a quiet setting away from the everyday.
Location
Clervaux is a town in the Luxembourg Ardennes, nestled in a wooded valley around a twelfth-century castle and a striking neo-Romanesque parish church. It is reachable by direct train from Luxembourg City in about one hour.
Program
Talks given by doctoral candidates are 25 minutes long; lectures by invited speakers consist of two 30-minute sessions. The Lean tutorial (sessions Lean 1 to Lean 8) is given by Florent Schaffhauser. Titles and abstracts of all talks are available on the Abstracts page.
| Sun 31 May | Mon 1 Jun | Tue 2 Jun | Wed 3 Jun | Thu 4 Jun | Fri 5 Jun | |
|---|---|---|---|---|---|---|
| 08:00–09:00 | — | Breakfast | Breakfast | Breakfast | Breakfast | Breakfast |
| 09:00–09:30 | — | Discussions | Belmans | Discussions | Despré | Discussions |
| 09:30–10:00 | — | Welcome, GRACE | Discussions | Discussions | ||
| 10:00–10:30 | — | Veneziale | Fisch | Gehrunger | Lean 5 | Lean 7 |
| 10:30–11:00 | — | Tognetti | ||||
| 11:00–11:30 | — | Break | Break | Break | Break | Break |
| 11:30–12:00 | — | Benoist | Lean 1 | Lean 3 | Lean 6 | Lean 8 |
| 12:00–12:30 | — | Boeren | ||||
| 12:30–14:00 | — | Lunch, discussion | Lunch, discussion | Lunch, discussion | Lunch, discussion | Lunch, discussion |
| 14:00–15:00 | — | Discussion: experience with LLMs | Discussion: experience with LLMs | Discussion | Discussion | Discussion |
| 15:15–15:45 | — | Mahmoudian | Lean 2 | Lean 4 | Excursion | — |
| 15:45–16:15 | — | Lidgren | Excursion | — | ||
| 16:15–16:30 | — | Break | Break | Break | Excursion | — |
| 16:30–17:00 | — | Fernández Píriz | Page | Usula | Excursion | — |
| 17:00–17:30 | — | Hobohm | Excursion | — | ||
| 17:30–19:00 | Discussions | Discussions | Discussions | Discussions | Discussions | — |
| 19:00–20:30 | Dinner | Dinner | Dinner | Dinner | Dinner | — |
Titles and abstracts of the talks are listed on the Abstracts page.
The slides and files for the practical activities of the LEAN course can be found on Florent Schaffhauser's page here.