BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Thomas R. Murrills (The Mathlib Initiative\, a program of Renaissa nce Philanthropy) DTSTART:20260121T183000Z DTEND:20260121T190000Z DTSTAMP:20260420T025455Z UID:LT2026/26 DESCRIPTION:Title: Better living through metaprogramming: Solving the Goldblum Dilemma with c otools\nby Thomas R. Murrills (The Mathlib Initiative\, a program of R enaissance Philanthropy) as part of Lean Together 2026\n\n\nAbstract\nLean ’s metaprogramming promises powerful capabilities we’ve yet to dream o f\; aye\, there’s the rub.\n\nIn this talk\, we’ll imagine the future that Lean metaprogramming has the potential to bring\, while trying to rec kon with the library-scale burdens of complexity and maintenance that coul d come with it. We’ll conceptualize and explore the philosophy of “cot ools” as a means of healthily growing a library’s metaprogramming infr astructure while allowing our vision to thrive.\n\nConcretely\, we’ll al so introduce Skimmer\, a cotool currently in development\, as a taste of t he sort of library-scale manipulation that the metaprogramming of the futu re may soon bring. In doing so\, we’ll ask what opportunities are actual ly available to Lean metaprograms: what information does Lean create\, and when? How can we catch it\, and “skim” it off the surface? More gener ally\, 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?\n LOCATION:https://researchseminars.org/talk/LT2026/26/ END:VEVENT END:VCALENDAR