Leaning In! 2025
A workshop for the Lean community in & around Europe, Germany, and Berlin
A workshop for the Lean community in & around Europe, Germany, and Berlin
Join us for a day of collaboration and learning centered around the Lean programming language & proof assistant. Whether you're using Lean for mathematical proofs, functional programming, teaching, language specification, or system verification—in short, if you're using Lean!—this workshop offers a space to share ideas, learn new techniques, and connect with fellow enthusiasts.
Leaning In! is primarily an in-person event. However, a remote participation option is available.
Date: Thursday, March 13, 2025
Time: 9:00 AM - 5:00 PM
Venue: Spielfeld Digital Hub
Skalitzer Strasse 85/86
10997 Berlin
Germany
Capacity: 40 participants (If there is a lot of interest in the event, we will attempt to book a bigger room at the venue.)
The program is full, so the call for submissions is closed!
The logic underlying Lean does not know recursive functions, yet Lean users can define functions recursively. In this session we'll get to look at how Lean translates the user's specification into something that the logic understands, whether by structural recursion, well-founded recursion or the brand-new partial fixpoint strategy. We'll also see how this affects compiled code (namely not at all), and the difference between partial and unsafe.
This session will likely contain high amounts of improvised live-coding and benefit greatly from your questions, suggestions and discussions.
Instruction Set Architectures (ISA) are abstract models which specify the behavior of processors at the machine code level. They are now specified using custom programming languages such as Sail and ASL instead of being specified using prose. I will present a new, work-in-progress backend for the Sail compiler, which translates the ISA specifications into Lean code. I will then sketch how this fits in existing formalization efforts such as Lean-MLIR, a formalization of the MLIR intermediate representation and compiler infrastructure in Lean.
Fast Discrete Fourier Transforms are key algorithms in signal processing and big integer computations. Implementation of the plain definition however would result in quadratic runtime. Linear-logarithmic runtime is always possible, but you need a toolbox of algorithms tailored to different vector sizes. The choice of the algorithm depends on whether the vector size is prime, composite with coprime factors, or arbitrary composite. It also depends on considerations of data locality. There is a fallback method, when all the other approaches are too slow.
As a toy project for learning Lean, I implemented the common Fast Fourier Transform algorithms and proved their correctness.
Drinfeld modules are an object of interest in Number Theory. I have been working on formalizing basic properties of this object with María Inés de Frutos Fernández. The project is very much WIP. I'll talk about some difficulties we encountered with Lean and Mathlib, the mathematics that we needed the develop as well as how we plan to tackle the remaining tasks.
Category theory is an abstract framework used to study mathematical structures and their relationships. It has significantly influenced many areas of mathematics and theoretical computer science, such as abstract algebra and type theory. However, traditional category theory cannot capture the intricacies of all mathematical domains, resulting in the development of a theory of "higher categories". This advanced theory has become pivotal in modern research areas such as algebraic topology and homotopy type theory. Unfortunately, these advancements come at a significant price, as higher category theory is notoriously technical and susceptible to errors. The formalization of higher category theory presents a promising solution to address these challenges. This has resulted in several formalization efforts, leveraging a variety of proof assistants, including a recent project in Lean, commenced by Emily Riehl: the ∞-Cosmos project. In this talk, I will explore the merits and limitations of formalizing higher category theory within Lean, share my experience with the ∞-Cosmos project, and highlight some technical obstacles that hinder further advancements. No prior knowledge of (higher) category theory will be assumed for this talk.
Bordism theory is perhaps the simplest example of an extraordinary homology theory. Proving the Eilenberg-Steenrod axioms is particularly simple (unlike for e.g. singular homology). It is used e.g. in the proof of the Hirzebruch signature theorem, which is one ingredient for the existence of exotic spheres. I have been working on formalising the basics of (unoriented) bordism theory: this is both beautiful mathematics and an interesting test of mathlib's differential geometry library. I will explain the main ideas, and speak about the insights and challenges from formalisation: as so often, finding the right definition is less obvious than it seems. This is ongoing work. No prior knowledge in differential geometry will be assumed.
We model two player turn based games such as Chomp and Tic-Tac-Toe. We define the notion of (winning) strategies and show that under the right conditions, games must have winning strategies (Zermelo's theorem). We apply these notions to the games of Chomp and Tic-Tac-Toe and prove some fun results. The work can be found here.
As Lean does not support coinductive types directly, formalizing infinite lists and infinite trees requires some "creativity". As a byproduct of one of our ongoing works, we formalized possibly infinite trees of bounded degree in Lean. In this workshop, we will reproduce this idea and present the definition from scratch (even without mathlib). We will work towards showing a special case of König's Lemma: if each branch in such a tree is finite, then there are only finitely many branches.
We have a reservation at the nearby 3 Schwestern restaurant. When registering, indicate whether you'd like to join us there! Here's their menu (in German).
The workshop is over, so registration is closed!
The proceedings of Leaning In! will take place under the Racket Friendly Environment Policy, with, of course, the understanding that the Leaning In! organizers, rather than Racket management, are in charge of this event.
Leaning In! pairs well with BOBKonf, which takes places in Berlin the day after Leaning In!
BOB asks: What if we use the best for a change?
You'll find BOB to be a pretty Lean-friendly place. See you there!
To help keep costs down, we appreciate any support you can offer. Sponsors will be proudly listed here and called out on-site. To sponsor Leaning In! 2025, just go here.