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.

The event is in-per­son only. A re­mote par­tic­i­pa­tion op­tion is, un­for­tu­nate­ly, not 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.

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

10:30 – 11:00

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:00 – 11:30

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

11:30 – 12:00

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:00 – 12:30

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

The pro­gram is still in de­vel­op­ment—stay tuned! Did you see the Call for Sub­mis­sions?

Reg­is­tra­tion

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!

(NB: The reg­is­tra­tion form and the call for sub­mis­sion form are the same thing. If you want to reg­is­ter but don't want to present, you can in­di­cate that on the web page.)

What to Bring

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.