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: 40 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

The pro­gram is full, so the call for sub­mis­sions is closed!

Work­shop For­mat

Pro­gram

Doors open

09:00 – 09:20

Open­ing re­marks & set­up

09:20 – 09:30

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

09:30 – 10:00
[slides]

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.

Bring­ing ISA se­man­tics to Lean and Lean-MLIR

10:00 – 10:30
[slides]

Léo Ste­fanesco

In­struc­tion Set Ar­chi­tec­tures (ISA) are ab­stract mod­els which spec­i­fy the be­hav­ior of pro­ces­sors at the ma­chine code lev­el. They are now spec­i­fied us­ing cus­tom pro­gram­ming lan­guages such as Sail and ASL in­stead of be­ing spec­i­fied us­ing prose. I will present a new, work-in-progress back­end for the Sail com­pil­er, which trans­lates the ISA spec­i­fi­ca­tions into Lean code. I will then sketch how this fits in ex­ist­ing for­mal­iza­tion ef­forts such as Lean-MLIR, a for­mal­iza­tion of the MLIR in­ter­me­di­ate rep­re­sen­ta­tion and com­pil­er in­fra­struc­ture in Lean.

Cof­fee

10:30 – 11:00

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

11:00 – 11:30
[slides]

Hen­ning Thiele­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 high­er cat­e­gories

12:00 – 12:30
[slides]

Nima Rasekh

Cat­e­go­ry the­o­ry is an ab­stract frame­work used to study math­e­mat­i­cal struc­tures and their re­la­tion­ships. It has sig­nif­i­cant­ly in­flu­enced many ar­eas of math­e­mat­ics and the­o­ret­i­cal com­put­er sci­ence, such as ab­stract al­ge­bra and type the­o­ry. How­ev­er, tra­di­tion­al cat­e­go­ry the­o­ry can­not cap­ture the in­tri­ca­cies of all math­e­mat­i­cal do­mains, re­sult­ing in the de­vel­op­ment of a the­o­ry of high­er cat­e­gories. This ad­vanced the­o­ry has be­come piv­otal in mod­ern re­search ar­eas such as al­ge­bra­ic topol­o­gy and ho­mo­topy type the­o­ry. Un­for­tu­nate­ly, these ad­vance­ments come at a sig­nif­i­cant price, as high­er cat­e­go­ry the­o­ry is no­to­ri­ous­ly tech­ni­cal and sus­cep­ti­ble to er­rors. The for­mal­iza­tion of high­er cat­e­go­ry the­o­ry presents a promis­ing so­lu­tion to ad­dress these chal­lenges. This has re­sult­ed in sev­er­al for­mal­iza­tion ef­forts, lever­ag­ing a va­ri­ety of proof as­sis­tants, in­clud­ing a re­cent project in Lean, com­menced by Emi­ly Riehl: the ∞-Cos­mos project. In this talk, I will ex­plore the mer­its and lim­i­ta­tions of for­mal­iz­ing high­er cat­e­go­ry the­o­ry with­in Lean, share my ex­pe­ri­ence with the ∞-Cos­mos project, and high­light some tech­ni­cal ob­sta­cles that hin­der fur­ther ad­vance­ments. No pri­or knowl­edge of (high­er) cat­e­go­ry the­o­ry will be as­sumed for this talk.

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

12:30 – 14:00

Proof clin­ic

14:00 – 15:00

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!

Cof­fee

15:00 – 15:30

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

15:30 – 16:00

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:00 – 16:30
[slides]

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.

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

16:30 – 17:00
[slides]

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.

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

The work­shop is over, so reg­is­tra­tion is closed!

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.