Better living through metaprogramming: Solving the Goldblum Dilemma with cotools

Abstract: Lean’s metaprogramming promises powerful capabilities we’ve yet to dream of; aye, there’s the rub.

In this talk, we’ll imagine the future that Lean metaprogramming has the potential to bring, while trying to reckon with the library-scale burdens of complexity and maintenance that could come with it. We’ll conceptualize and explore the philosophy of “cotools” as a means of healthily growing a library’s metaprogramming infrastructure while allowing our vision to thrive.

Concretely, we’ll also introduce Skimmer, a cotool currently in development, as a taste of the sort of library-scale manipulation that the metaprogramming of the future may soon bring. In doing so, we’ll ask what opportunities are actually available to Lean metaprograms: what information does Lean create, and when? How can we catch it, and “skim” it off the surface? More generally, what challenges do we face in creating more powerful functionality? And how might our metaprograms overcome them—without us being overcome by them in turn?

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026