Leaning In! 2025

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.

In­struc­tion Set Ar­chi­tec­tures (ISA) are ab­stract mod­els which spec­i­fy the be­hav­ior of proces­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.

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.

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.

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.

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.

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­melo'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.

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.