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.

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.

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".