Lean­ing In! 2025

Banner image for Leaning In!: A universal and existential quantifier, leaning to the right, enclosed within a rhombus that also skews to the right

A work­shop for the Lean com­mu­ni­ty in & around Eu­rope, Ger­many, and Berlin

About

Join us for a day of col­lab­o­ra­tion and learn­ing cen­tered around the Lean pro­gram­ming lan­guage & proof as­sis­tant. Whether you’re us­ing Lean for math­e­mat­i­cal proofs, func­tion­al pro­gram­ming, teach­ing, lan­guage spec­i­fi­ca­tion, or sys­tem ver­i­fi­ca­tion—in short, if you’re us­ing Lean!—this work­shop of­fers a space to share ideas, learn new tech­niques, and con­nect with fel­low en­thu­si­asts.

Lean­ing In! is pri­mar­i­ly an in-per­son event. How­ev­er, a re­mote par­tic­i­pa­tion op­tion is avail­able.

De­tails

Date Thurs­day, March 13, 2025

Time 9:00 AM - 5:00 PM

Venue:
Skalitzer Strasse 85/86
10997 Berlin
Ger­many

Ca­pac­i­ty: 25 par­tic­i­pants
(If there is a lot of in­ter­est in the event, we will at­tempt to book a big­ger room at the venue.)

Call for Sub­mis­sions

We wel­come pro­pos­als for talks and demon­stra­tions across the spec­trum of Lean ap­pli­ca­tions, from math­e­mat­i­cal proofs to in­dus­tri­al ap­pli­ca­tions. Share your ex­pe­ri­ences, tech­niques, and in­sights with the com­mu­ni­ty.

Please sub­mit your pro­pos­al by Fri­day, March 7, 2025, in­clud­ing a brief de­scrip­tion (max 200 words) and any tech­ni­cal re­quire­ments.

Sub­mit Your Pro­pos­al

(NB: The reg­is­tra­tion form and the call for sub­mis­sion form are the same thing.)

Work­shop For­mat

Pro­gram

Open­ing re­marks & set­up

09:00 – 09:30

Re­cur­sive de­f­i­n­i­tions

09:30 – 10:30

Joachim Bre­it­ner

The log­ic un­der­ly­ing Lean does not know re­cur­sive func­tions, yet Lean users can de­fine func­tions re­cur­sive­ly. In this ses­sion we’ll get to look at how Lean trans­lates the user’s spec­i­fi­ca­tion into some­thing that the log­ic un­der­stands, whether by struc­tur­al re­cur­sion, well-found­ed re­cur­sion or the brand-new par­tial fix­point strat­e­gy. We’ll also see how this af­fects com­piled code (name­ly not at all), and the dif­fer­ence be­tween par­tial and un­safe.

This ses­sion will like­ly con­tain high amounts of im­pro­vised live-cod­ing and ben­e­fit great­ly from your ques­tions, sug­ges­tions and dis­cus­sions.

Cof­fee

10:30 – 11:00

Proof­ing cor­rect­ness of Fast Dis­crete Fouri­er trans­forms

11:00 – 11:30

Hen­ning Thiel­mann

Fast Dis­crete Fouri­er Trans­forms are key al­go­rithms in sig­nal pro­cess­ing and big in­te­ger com­pu­ta­tions. Im­ple­men­ta­tion of the plain de­f­i­n­i­tion how­ev­er would re­sult in qua­drat­ic run­time. Lin­ear-log­a­rith­mic run­time is al­ways pos­si­ble, but you need a tool­box of al­go­rithms tai­lored to dif­fer­ent vec­tor sizes. The choice of the al­go­rithm de­pends on whether the vec­tor size is prime, com­pos­ite with co­prime fac­tors, or ar­bi­trary com­pos­ite. It also de­pends on con­sid­er­a­tions of data lo­cal­i­ty. There is a fall­back method, when all the oth­er ap­proach­es are too slow.

As a toy project for learn­ing Lean, I im­ple­ment­ed the com­mon Fast Fouri­er Trans­form al­go­rithms and proved their cor­rect­ness.

For­mal­iza­tion of Drin­feld Mod­ules

11:30 – 12:00

Xavier Généreux

Drin­feld mod­ules are an ob­ject of in­ter­est in Num­ber The­o­ry. I have been work­ing on for­mal­iz­ing ba­sic prop­er­ties of this ob­ject with María Inés de Fru­tos Fer­nán­dez. The project is very much WIP. I’ll talk about some dif­fi­cul­ties we en­coun­tered with Lean and Math­lib, the math­e­mat­ics that we need­ed the de­vel­op as well as how we plan to tack­le the re­main­ing tasks.

For­mal­iz­ing Pos­si­bly In­fi­nite Trees of Bound­ed De­gree

12:00 – 12:30

Lukas Ger­lach

As Lean does not sup­port coin­duc­tive types di­rect­ly, for­mal­iz­ing in­fi­nite lists and in­fi­nite trees re­quires some "cre­ativ­i­ty". As a byprod­uct of one of our on­go­ing works, we for­mal­ized pos­si­bly in­fi­nite trees of bound­ed de­gree in Lean. In this work­shop, we will re­pro­duce this idea and present the de­f­i­n­i­tion from scratch (even with­out math­lib). We will work to­wards show­ing a spe­cial case of König’s Lem­ma: if each branch in such a tree is fi­nite, then there are only fi­nite­ly many branch­es.

For­mal­iz­ing IEEE 754 dec­i­mal float­ing-point arith­metic in Lean

12:30 – 13:00

Jesse Ala­ma

IEEE 754 is a the wide­ly de­ployed stan­dard for float­ing-point num­bers and their arith­metic. Usu­al­ly, by float­ing-point num­ber we un­der­stand bi­na­ry (base-2) float­ing-point rep­re­sen­ta­tions. IEEE 754 stan­dard­izes dec­i­mal (base-10) float­ing-point arith­metic, too. As part of the ef­fort to add ex­act dec­i­mal num­bers to JavaScript, we are for­mal­iz­ing this part of IEEE 754 in Lean. Come find out what for­mal­iz­ing a pro­gram­ming lan­guage spec text looks like!

Lunch at Mark­thalle Neun (or wher­ev­er you wish!)

13:00 – 14:30

Proof clin­ic

14:30 – 15:30

Are you stuck with a proof? Can’t fig­ure out how to get a fea­ture to work? Don’t know how to for­mal­ize some­thing? Don’t get the er­ror Lean keeps emit­ting? Are you sor­ry about that sor­ry? In the Proof Clin­ic we’ll work to­geth­er to try to get you un­stuck. No promis­es, but we’ll do our lev­el best to get you un­stuck!

Cof­fee

15:30 – 16:00

For­mal­is­ing bor­dism the­o­ry

16:00 – 16:30

Michael Roth­gang

Bor­dism the­o­ry is per­haps the sim­plest ex­am­ple of an ex­tra­or­di­nary ho­mol­o­gy the­o­ry. Prov­ing the Eilen­berg-Steen­rod ax­ioms is par­tic­u­lar­ly sim­ple (un­like for e.g. sin­gu­lar ho­mol­o­gy). It is used e.g. in the proof of the Hirze­bruch sig­na­ture the­o­rem, which is one in­gre­di­ent for the ex­is­tence of ex­ot­ic spheres. I have been work­ing on for­mal­is­ing the ba­sics of (un­ori­ent­ed) bor­dism the­o­ry: this is both beau­ti­ful math­e­mat­ics and an in­ter­est­ing test of math­lib’s dif­fer­en­tial geom­e­try li­brary. I will ex­plain the main ideas, and speak about the in­sights and chal­lenges from for­mal­i­sa­tion: as so of­ten, find­ing the right de­f­i­n­i­tion is less ob­vi­ous than it seems. This is on­go­ing work. No pri­or knowl­edge in dif­fer­en­tial geom­e­try will be as­sumed.

Com­bi­na­to­r­i­al and po­si­tion­al games in Lean

16:30 – 17:00

Yves Jäck­le

We mod­el two play­er turn based games such as Chomp and Tic-Tac-Toe. We de­fine the no­tion of (win­ning) strate­gies and show that un­der the right con­di­tions, games must have win­ning strate­gies (Zer­me­lo’s the­o­rem). We ap­ply these no­tions to the games of Chomp and Tic-Tac-Toe and prove some fun re­sults. The work can be found here.

The pro­gram is still in de­vel­op­ment—stay tuned! Have some­thing Lean-y that you’d like to present? Take a look at the Call for Sub­mis­sions?

Din­ner (op­tion­al)

We have a reser­va­tion at the near­by 3 Schwest­ern restau­rant. When reg­is­ter­ing, in­di­cate whether you’d like to join us there! Here’s their menu (in Ger­man).

Reg­is­tra­tion

In-per­son Reg­is­tra­tion Fee: 40 EUR

Reg­is­tra­tion is re­quired due to lim­it­ed ca­pac­i­ty at our venue. Please reg­is­ter ear­ly to se­cure your spot! For those who can’t make it to Berlin, a re­mote reg­is­tra­tion op­tion (Zoom call) will be avail­able.

(NB: The in-per­son reg­is­tra­tion form and the call for sub­mis­sion form are the same thing. If you want to at­tend in per­son but don’t want to present any­thing, just leave the ti­tle & ab­stract part of the form blank.)

What to Bring

Friend­ly Pol­i­cy

The pro­ceed­ings of Lean­ing In! will take place un­der the Rack­et Friend­ly En­vi­ron­ment Pol­i­cy, with, of course, the un­der­stand­ing that the Lean­ing In! or­ga­niz­ers, rather than Rack­et man­age­ment, are in charge of this event.

Part­ners

Logo for BOBKonf

Lean­ing In! pairs well with , which takes places in Berlin the day af­ter Lean­ing In!

BOB asks: What if we use the best for a change? You’ll find BOB to be a pret­ty Lean-friend­ly place. See you there!

Spon­sors

To help keep costs down, we ap­pre­ci­ate any sup­port you can of­fer. Spon­sors will be proud­ly list­ed here and called out on-site. To spon­sor Lean­ing In! 2025, just go here.