Leaning In! 2026

Over the past year, the Lean FRO has been mak­ing a big push to­wards mak­ing Lean a great gen­er­al-pur­pose pro­gram­ming lan­guage that you can use to de­vel­op for­mal­ly ver­i­fied pro­duc­tion-ready soft­ware. In this pre­sen­ta­tion, I will give an overview over the many re­cent in­no­va­tions in Lean that are rel­e­vant for soft­ware de­vel­op­ers, in­clud­ing im­prove­ments to the com­pil­er, the stan­dard li­brary, and the ver­i­fi­ca­tion in­fra­struc­ture for monadic pro­grams.

CSLib is an open-source frame­work de­signed as the com­put­er sci­ence coun­ter­part to Lean's in­flu­en­tial Math­lib, en­abling for­mal the­o­rem prov­ing and ver­i­fied code de­vel­op­ment across com­put­er sci­ence do­mains. In this talk, I will dis­cuss CSLib in more de­tail, as well as cur­rent on­go­ing projects and ac­tiv­i­ties.

Proof scripts pro­duced by AI sys­tems such as Aris­to­tle are of­ten un­nec­es­sar­i­ly ver­bose or oth­er­wise uni­d­iomat­ic. I present a work-in-progress frame­work for op­ti­mis­ing these proof scripts, e.g. by re­mov­ing re­dun­dant steps. The frame­work sup­ports both pure­ly syn­tac­tic op­ti­mi­sa­tions and se­man­ti­cal­ly guid­ed ones that rely on in­for­ma­tion from an ear­li­er elab­o­ra­tion. Re­peat­ed elab­o­ra­tion leads to per­for­mance con­cerns that we par­tial­ly mit­i­gate.

How can math­e­mati­cians con­tribute to the im­prove­ment of AI sys­tems by do­ing maths? The Proof­Bench Ini­tia­tive aims to build a bench­mark suite for math­e­mat­i­cal proof ver­i­fi­ca­tion and gen­er­a­tion, en­abling mean­ing­ful test­ing of AI sys­tems. The project fo­cus­es on us­ing Lean to for­malise prob­lem state­ments and in­ter­me­di­ate re­sults from re­search math­e­mat­ics.

The Proof­Bench Ini­tia­tive is in its ear­ly stages. In this talk, we will out­line the goals of the project, de­scribe the types of con­tri­bu­tions that are need­ed, and ex­plain how in­ter­est­ed math­e­mati­cians can get in­volved as the project de­vel­ops.

An MCP serv­er con­nect­ing AI agents to the Lean 4 the­o­rem prover via the Lan­guage Serv­er Pro­to­col. This talk cov­ers the Lean lan­guage serv­er ba­sics, how the MCP serv­er in­ter­acts with it, and the key tools it pro­vides. In­cludes a live demo in VS Code.

At Cryspen, we are de­vel­op­ing a tool­chain called Hax to ver­i­fy Rust code with Lean. The tool tran­spiles an­no­tat­ed Rust code into monadic Lean code, which can then be ver­i­fied with the ver­i­fi­ca­tion in­fra­struc­ture de­vel­oped by the Lean FRO. I will de­scribe the tool and show how we use the tool to ver­i­fy Rust im­ple­men­ta­tions of mod­ern cryp­to­graph­ic al­go­rithms such as SHA-3 and ML-KEM.

In this talk I will out­line the choic­es made and chal­lenges faced in for­mal­iz­ing en­er­gy-based neur­al net­works in Lean 4, high­light­ing the dif­fer­ent lay­ers re­quired for a 'three-di­men­sion­al' re­con­struc­tion of the phys­i­cal and math­e­mat­i­cal lay­ers un­der­ly­ing these mod­els, as well as how to ex­e­cute these spec­i­fi­ca­tions with com­putable re­als and floats, how to con­nect them mean­ing­ful­ly to mod­ern trans­former-based ar­chi­tec­tures and how cur­rent physics re­search in spin glass­es could be mean­ing­ful­ly for­mal­ized with­in the same frame­work, by this lay­ered ap­proach.

The con­cept of a Tur­ing ma­chine ex­ists in Math­lib, but only as a sim­ple one-tape ver­sion. In this talk, I will ex­plain my de­sign choic­es in ex­tend­ing it to a mul­ti-tape ver­sion with the idea to for­mal­ize space-bound­ed com­plex­i­ty the­o­ry. On top of this foun­da­tion, I built a tool­box of com­pu­ta­tion prim­i­tives and com­po­si­tion con­nec­tives that al­lows build­ing com­plex al­go­rithms and rea­son about their space and time re­quire­ments. The mo­ti­vat­ing goal at the hori­zon is to for­mal­ize Ryan William's 2025 re­sult "Sim­u­lat­ing Time With Square-Root Space".

The ProofWid­gets li­brary of Lean (https://github.com/lean­prover-com­mu­ni­ty/ProofWid­gets4) sets up the nec­es­sary in­fra­struc­ture to al­low cus­tom web code to be dis­played in the in­foview and pro­vides ab­strac­tions, datas­truc­tures and no­ta­tion that make this process more con­ve­nient. In par­tic­u­lar, it fea­tures a do­main-spe­cif­ic lan­guage that al­lows one to de­fine and ren­der pure Re­act code (i.e., code with no side ef­fects) in Lean us­ing id­iomat­ic JSX-like syn­tax. Ren­der­ing more com­pli­cat­ed Re­act com­po­nents re­quires writ­ing cus­tom Type­Script/JavaScript code in an ex­ter­nal file and read­ing it into Lean. In this talk, I will present some on­go­ing work that builds on top of the ProofWid­gets li­brary to al­low com­po­nents in­volv­ing cer­tain kinds of states and ef­fects to be de­fined and ren­dered from with­in Lean. As a pri­ma­ry ap­pli­ca­tion, I will present an "in­ter­ac­tive mon­ad", de­vel­oped joint­ly with Sid­dharth Bhat, that makes it pos­si­ble to de­fine mul­ti-turn in­ter­ac­tions where users can con­struct data in Lean by per­form­ing a se­ries of ac­tions in the in­foview.