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: 25 participants
(If there is a lot of interest in the event, we will attempt to book a bigger room at the venue.)
We welcome proposals for talks and demonstrations across the spectrum of Lean applications, from mathematical proofs to industrial applications. Share your experiences, techniques, and insights with the community.
Please submit your proposal by Friday, March 7, 2025, including a brief description (max 200 words) and any technical requirements.
Submit Your Proposal(NB: The registration form and the call for submission form are the same thing.)
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.
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.
floating-point numberwe understand binary (base-2) floating-point representations. IEEE 754 standardizes decimal (base-10) floating-point arithmetic, too. As part of the effort to add exact decimal numbers to JavaScript, we are formalizing this part of IEEE 754 in Lean. Come find out what formalizing a programming language spec text looks like!
sorry
? In the Proof Clinic we’ll work together to try to get you unstuck. No promises, but we’ll do our level best to get you unstuck!The program is still in development—stay tuned! Have something Lean-y that you’d like to present? Take a look at the Call for Submissions?
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).
Registration is required due to limited capacity at our venue. Please register early to secure your spot! For those who can’t make it to Berlin, a remote registration option (Zoom call) will be available.
(NB: The in-person registration form and the call for submission form are the same thing. If you want to attend in person but don’t want to present anything, just leave the title & abstract part of the form blank.)
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.