BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Johan Commelin (Mathlib Initiative\, Universiteit Utrecht)
DTSTART:20260119T141500Z
DTEND:20260119T144500Z
DTSTAMP:20260419T233655Z
UID:LT2026/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/1/">T
 he Mathlib Initiative: Scaling\, Infrastructure\, and Future Directions</a
 >\nby Johan Commelin (Mathlib Initiative\, Universiteit Utrecht) as part o
 f Lean Together 2026\n\n\nAbstract\nIn this talk\, we will review the prog
 ress of the Mathlib Initiative since its launch in September 2025. We’ll
  discuss the challenges that have come with Mathlib’s growth\, particula
 rly in managing review times\, documentation\, and ecosystem coordination.
  We’ll also cover the infrastructure improvements made to address these 
 issues\, including the editorial support and tools that have been put in p
 lace.\n\nLooking ahead\, we will outline our plans for 2026\, focusing on 
 how we aim to continue supporting the Mathlib community’s growth while k
 eeping the project sustainable and scalable. This includes ongoing efforts
  to improve the review process\, provide better resources for new contribu
 tors\, and enhance collaboration across different areas of formal mathemat
 ics.\n
LOCATION:https://researchseminars.org/talk/LT2026/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Vasilii Nesterov
DTSTART:20260119T144500Z
DTEND:20260119T151500Z
DTSTAMP:20260419T233655Z
UID:LT2026/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/2/">V
 erified computation of real asymptotics</a>\nby Vasilii Nesterov as part o
 f Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jonas van der Schaaf (Universität Münster)
DTSTART:20260119T151500Z
DTEND:20260119T154500Z
DTSTAMP:20260419T233655Z
UID:LT2026/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/3/">I
 nternal Projectivity of the Sequence Space in Lean</a>\nby Jonas van der S
 chaaf (Universität Münster) as part of Lean Together 2026\n\n\nAbstract\
 nThe theory of condensed mathematics has been well-explored in formalized 
 mathematics. In my master thesis\, I proved that the sequence space\, a co
 ndensed Abelian group describing null-sequences\, is internally projective
  in the category of light condensed abelian groups. I will discuss the pro
 of\, and what it is like for a relative beginner to prove a non-trivial th
 eorem in Lean.\n
LOCATION:https://researchseminars.org/talk/LT2026/3/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leopoldo Sarra (Axiomatic AI)
DTSTART:20260119T160000Z
DTEND:20260119T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/4/">T
 owards autoformalization for physics and engineering with Lean</a>\nby Leo
 poldo Sarra (Axiomatic AI) as part of Lean Together 2026\n\n\nAbstract\nWe
  strive to bring formal methods and interactive theorem provers like Lean 
 4 to the broader scientific community beyond mathematics. To ease its adop
 tion\, we are building reusable Lean libraries that formalize areas of sci
 ence using the main concepts that scientists and engineers actually apply 
 in practice\, such as dimensional analysis\, tolerances\, and approximatio
 ns.\n\nWe begin with physics domains that have a strong mathematical groun
 ding\, like quantum mechanics\, where we validate the correctness of the l
 ibraries on real use cases and problem sets (e. g. 700 problems from Galit
 ski et. al. 2013) to ensure their practical relevance and adoptability.\n\
 nFinally\, we are developing autoformalization AI agents to further boost 
 the adoption of formal methods in science and engineering. These agents wi
 ll have access to the libraries we build\, as well as Mathlib\, enabling t
 hem to help formalize real-world problems together with their proposed sol
 utions in the form of theorems. This allows us to certify the validity of 
 a given solution by converting it into a formal theorem and proving it thr
 ough our prover AI agents.\n
LOCATION:https://researchseminars.org/talk/LT2026/4/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Yaël Dillies (Stockholm University)
DTSTART:20260119T163000Z
DTEND:20260119T170000Z
DTSTAMP:20260419T233655Z
UID:LT2026/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/5/">H
 opf algebras\, affine group schemes and all of that</a>\nby Yaël Dillies 
 (Stockholm University) as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/5/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Leo de Moura (Lean FRO and AWS)
DTSTART:20260119T173000Z
DTEND:20260119T183000Z
DTSTAMP:20260419T233655Z
UID:LT2026/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/6/">T
 he State of Lean</a>\nby Leo de Moura (Lean FRO and AWS) as part of Lean T
 ogether 2026\n\n\nAbstract\n2025 has been a transformative year for Lean. 
 We released 12 versions (4.15–4.26)\, landing thousands of changes acros
 s proof automation\, the compiler\, tooling\, website\, documentation\, an
 d the standard library. The grind tactic shipped with SMT-style automation
  and interactive proof search. The new compiler replaced the old one\, clo
 sing long-standing issues and setting the foundation for future optimizati
 ons. Lake gained remote caching and a local artifact cache. The language s
 erver became significantly faster (3.5× autocomplete speedup)\, added sig
 nature help\, and introduced module hierarchy navigation. We released the 
 module system\, coinductive predicates\, and a monadic verification framew
 ork (mvcgen). The standard library expanded substantially with iterators\,
  async primitives\, and hundreds of new lemmas. We launched a new website 
 and published the Lean Language Reference\, both built with Verso. This ke
 ynote summarizes these accomplishments and outlines our priorities for 202
 6.\n
LOCATION:https://researchseminars.org/talk/LT2026/6/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Siddharth Bhat
DTSTART:20260119T183000Z
DTEND:20260119T190000Z
DTSTAMP:20260419T233655Z
UID:LT2026/7
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/7/">S
 ound & Complete Tactics for the Linear-Bitwise Fragment of Multi-Width Par
 ametric Bitvector Theory</a>\nby Siddharth Bhat as part of Lean Together 2
 026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/7/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Moritz Doll
DTSTART:20260120T123000Z
DTEND:20260120T130000Z
DTSTAMP:20260419T233655Z
UID:LT2026/8
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/8/">F
 ormalizing Schwartz functions and tempered distributions</a>\nby Moritz Do
 ll as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/8/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fabrizio Montesi
DTSTART:20260120T130000Z
DTEND:20260120T133000Z
DTSTAMP:20260419T233655Z
UID:LT2026/9
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/9/">C
 SLib: The Lean Computer Science Library</a>\nby Fabrizio Montesi as part o
 f Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/9/
END:VEVENT
BEGIN:VEVENT
SUMMARY:María Inés de Frutos Fernández
DTSTART:20260120T133000Z
DTEND:20260120T140000Z
DTSTAMP:20260419T233655Z
UID:LT2026/10
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/10/">
 Formalizing the universal divided power algebra</a>\nby María Inés de Fr
 utos Fernández as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/10/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lean Together Organizers
DTSTART:20260119T140000Z
DTEND:20260119T141500Z
DTSTAMP:20260419T233655Z
UID:LT2026/11
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/11/">
 Opening Remarks</a>\nby Lean Together Organizers as part of Lean Together 
 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/11/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260119T154500Z
DTEND:20260119T160000Z
DTSTAMP:20260419T233655Z
UID:LT2026/12
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/12/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/12/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260119T170000Z
DTEND:20260119T173000Z
DTSTAMP:20260419T233655Z
UID:LT2026/13
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/13/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/13/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260120T140000Z
DTEND:20260120T143000Z
DTSTAMP:20260419T233655Z
UID:LT2026/14
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/14/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/14/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Ullrich (Lean FRO)
DTSTART:20260120T143000Z
DTEND:20260120T150000Z
DTSTAMP:20260419T233655Z
UID:LT2026/15
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/15/">
 The Lean module system</a>\nby Sebastian Ullrich (Lean FRO) as part of Lea
 n Together 2026\n\n\nAbstract\nThe module system is a new extension of the
  Lean language that allows for more control over the public interface of L
 ean files\, considerably increasing robustness and scalability of librarie
 s in multiple aspects. In this talk\, I will cover the basics of the modul
 e system and what impact we are already seeing from its adoption in Mathli
 b and beyond.\n\nMore info:\n* https://lean-lang.org/doc/reference/latest/
 Source-Files-and-Modules/#module-scopes\n* https://drive.google.com/file/d
 /1AyaYBwnYON_bq3aWjS-Nr3b4vne7c4SJ/view ("Optimizing Lean Libraries using 
 the Module System" starts at 1:06:25)\n
LOCATION:https://researchseminars.org/talk/LT2026/15/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Stefan Kebekus
DTSTART:20260120T150000Z
DTEND:20260120T153000Z
DTSTAMP:20260419T233655Z
UID:LT2026/16
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/16/">
 Project VD: Formalizing Value Distribution Theory of Complex Analysis</a>\
 nby Stefan Kebekus as part of Lean Together 2026\n\n\nAbstract\nWe present
  "Project VD"\, an effort to formalize value distribution theory in the Le
 an theorem prover. Pioneered by Nevanlinna (and others) in the 1920s\, the
  theory studies how complex-analytic and meromorphic functions distribute 
 their values\, providing a quantitative measure of their complexity. Beyon
 d its intrinsic interest\, the theory gained wider significance after Vojt
 a found surprising connections between complex analysis and Diophantine ge
 ometry.\n\nThis talk will briefly introduce the main objects and report on
  the formalization work completed so far. Finally\, I would like to pose s
 everal open design questions that have emerged during this project\, hopin
 g to start a discussion in the community.\n
LOCATION:https://researchseminars.org/talk/LT2026/16/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260120T153000Z
DTEND:20260120T160000Z
DTSTAMP:20260419T233655Z
UID:LT2026/17
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/17/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/17/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sebastian Graf (Lean FRO)
DTSTART:20260120T160000Z
DTEND:20260120T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/18
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/18/">
 Simpler $\\texttt{do}$ proofs with $\\texttt{mvcgen}$</a>\nby Sebastian Gr
 af (Lean FRO) as part of Lean Together 2026\n\n\nAbstract\nSince last year
 \, $\\texttt{Std}$ features $\\texttt{mvcgen}$\, a new experimental tactic
  that implements a monadic verification condition generator. It breaks dow
 n a goal involving a program written using Lean's imperative $\\texttt{do}
 $ notation into a number of smaller $\\textit{verification conditions}$ th
 at are sufficient to prove the goal.\n\nIn this talk\, we will go through 
 a couple of examples that show how $\\texttt{mvcgen}$ enables compositiona
 l reasoning where previous tactics fall short and have a look at its seman
 tic foundations.\n
LOCATION:https://researchseminars.org/talk/LT2026/18/
END:VEVENT
BEGIN:VEVENT
SUMMARY:David Ledvinka
DTSTART:20260120T163000Z
DTEND:20260120T170000Z
DTSTAMP:20260419T233655Z
UID:LT2026/19
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/19/">
 Formalization of Brownian Motion in Lean</a>\nby David Ledvinka as part of
  Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/19/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Harry Goldstein (University at Buffalo\, SUNY)
DTSTART:20260120T170000Z
DTEND:20260120T173000Z
DTSTAMP:20260419T233655Z
UID:LT2026/20
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/20/">
 Metaprogramming the Next Generation of Testing Tools</a>\nby Harry Goldste
 in (University at Buffalo\, SUNY) as part of Lean Together 2026\n\n\nAbstr
 act\nLean is an incredible platform for mathematics\, but it is also an ex
 tremely capable programming language. By combining dependent types with a 
 state-of-the-art metaprogramming system\, Lean enables new approaches to w
 riting everyday programs.\n\nIn this talk\, I describe work that my collea
 gues and I have done over the last year that uses metaprogramming in Lean 
 to build new tools for automated testing. I'll demonstrate how Lean's proo
 f system can be repurposed as a system for interactive program synthesis\,
  and I'll show off some other interactive programming interfaces that woul
 d require far more work to implement in other languages.\n\nI hope that my
  talk will provide a glimpse of a new generation of testing tools and insp
 ire others to consider the expressive power of Lean in other programming d
 omains.\n
LOCATION:https://researchseminars.org/talk/LT2026/20/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Markus Himmel\, Sofia Rodrigues
DTSTART:20260121T160000Z
DTEND:20260121T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/21
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/21/">
 What's new in the Lean standard library</a>\nby Markus Himmel\, Sofia Rodr
 igues as part of Lean Together 2026\n\n\nAbstract\nThe Lean standard libra
 ry contains the basic concepts that underpin all Lean formalization and pr
 ogramming projects\, like logical connectives and natural numbers. It also
  contains fundamental building blocks for writing real-world software in L
 ean\, like high-quality implementations of data structures and primitives 
 for parallel programming. In 2025\, the Lean standard library team added m
 any new features that are essential for building production-ready software
  in Lean. We will go over the new features and show how they make Lean an 
 even more powerful tool for writing general-purpose (verified) software an
 d\, of course\, metaprograms.\n
LOCATION:https://researchseminars.org/talk/LT2026/21/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260121T163000Z
DTEND:20260121T170000Z
DTSTAMP:20260419T233655Z
UID:LT2026/22
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/22/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/22/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Jovan Gerbscheid (University of Cambridge)
DTSTART:20260121T170000Z
DTEND:20260121T173000Z
DTSTAMP:20260419T233655Z
UID:LT2026/23
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/23/">
 Writing proofs by clicking</a>\nby Jovan Gerbscheid (University of Cambrid
 ge) as part of Lean Together 2026\n\n\nAbstract\nIn this talk I will prese
 nt a prototype system that allows you to construct a Lean proof without ty
 ping any tactics or lemmas\, by simply clicking in the infoview. This buil
 ds upon my work on the `rw??` tactic that is in mathlib. This kind of tool
  is very useful for writing proofs\, especially to beginners\, and it woul
 d also make a great addition to the natural number game.\n\nYou can try `#
 infoview_search` yourself. It can be found at https://github.com/JovanGerb
 /infoview_search\n
LOCATION:https://researchseminars.org/talk/LT2026/23/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sophie Morel (CNRS/ENS de Lyon)
DTSTART:20260121T173000Z
DTEND:20260121T180000Z
DTSTAMP:20260419T233655Z
UID:LT2026/24
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/24/">
 Nori's construction in Lean\, or the many ways that a formalization projec
 t can fail.</a>\nby Sophie Morel (CNRS/ENS de Lyon) as part of Lean Togeth
 er 2026\n\n\nAbstract\nNori's construction\, also known as Nori's universa
 l factorization\, is a 2-universal construction in category theory. Though
  it looks very abstract and can be deduced from existing results in a few 
 lines\, it underlies the construction of the far from trivial category of 
 Nori motives.\nThe goal of this talk is to briefly explain what Nori's con
 struction is and why I wanted to formalize it\, then to report on the many
  things that went wrong (and a couple that went right). \nFamiliarity with
  categories would be helpful to follow the details.\n
LOCATION:https://researchseminars.org/talk/LT2026/24/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260121T180000Z
DTEND:20260121T183000Z
DTSTAMP:20260419T233655Z
UID:LT2026/25
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/25/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/25/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Thomas R. Murrills (The Mathlib Initiative\, a program of Renaissa
 nce Philanthropy)
DTSTART:20260121T183000Z
DTEND:20260121T190000Z
DTSTAMP:20260419T233655Z
UID:LT2026/26
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/26/">
 Better living through metaprogramming: Solving the Goldblum Dilemma with c
 otools</a>\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
BEGIN:VEVENT
SUMMARY:Sidharth Hariharan\, Seewoo Lee\, Chris Birkbeck (Carnegie Mellon\
 , UC Berkeley\, University of East Anglia)
DTSTART:20260121T190000Z
DTEND:20260121T193000Z
DTSTAMP:20260419T233655Z
UID:LT2026/27
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/27/">
 Progress on the Sphere Packing Project</a>\nby Sidharth Hariharan\, Seewoo
  Lee\, Chris Birkbeck (Carnegie Mellon\, UC Berkeley\, University of East 
 Anglia) as part of Lean Together 2026\n\n\nAbstract\nWe will discuss the o
 ngoing effort to formalise Maryna Viazovska's Fields medal work on Sphere 
 Packings in $8$ dimensions. We will recap the main achievements so far and
  the problems that still remain.\n
LOCATION:https://researchseminars.org/talk/LT2026/27/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260121T193000Z
DTEND:20260121T200000Z
DTSTAMP:20260419T233655Z
UID:LT2026/28
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/28/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/28/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Kontorovich (Rutgers University)
DTSTART:20260121T200000Z
DTEND:20260121T203000Z
DTSTAMP:20260419T233655Z
UID:LT2026/29
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/29/">
 Teaching Real Analysis as a Video Game</a>\nby Alex Kontorovich (Rutgers U
 niversity) as part of Lean Together 2026\n\n\nAbstract\nWe will discuss te
 aching with Real Analysis\, The Game\, available here: https://adam.math.h
 hu.de/#/g/AlexKontorovich/RealAnalysisGame\n
LOCATION:https://researchseminars.org/talk/LT2026/29/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Chris Henson (Drexel University)
DTSTART:20260121T203000Z
DTEND:20260121T210000Z
DTSTAMP:20260419T233655Z
UID:LT2026/30
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/30/">
 Proof Automation and Metaprogramming in CSLib: Locally Nameless Lambda Cal
 culi</a>\nby Chris Henson (Drexel University) as part of Lean Together 202
 6\n\n\nAbstract\nThis talk will discuss CSLib's locally nameless formaliza
 tion of lambda calculi\, which currently includes STLC and System F with s
 ubtyping. While this is a well-established style of formalization\, we use
  Lean's new proof automation features and metaprogramming in ways that are
  interesting to consider. We make heavy use of the grind tactic\, allowing
  us to easily reuse existing Mathlib infrastructure for typing contexts an
 d in general enable a succinct style that is approximately 45% fewer LoC t
 han comparable formalizations. Metaprogramming has also been useful\, allo
 wing us to standardize certain notations and develop a single term elabora
 tor for selecting fresh variables that does not require specialization for
  each type system.\n
LOCATION:https://researchseminars.org/talk/LT2026/30/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Wojciech Różowski (Lean FRO)
DTSTART:20260122T150000Z
DTEND:20260122T153000Z
DTSTAMP:20260419T233655Z
UID:LT2026/31
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/31/">
 Coinductive predicates in Lean</a>\nby Wojciech Różowski (Lean FRO) as p
 art of Lean Together 2026\n\n\nAbstract\nCoinduction\, the mathematical du
 al of induction\, is a fundamental proof principle in computer science\, e
 ssential for reasoning about infinite structures\, concurrent systems\, an
 d compiler correctness. While full coinductive data support in proof assis
 tants typically requires foundational support and careful considerations\,
  such as syntactic guardedness checking\, focusing on the simpler case of 
 coinductive predicates can recover many important use cases. This is suffi
 cient for defining concepts like bisimulations and other coinductive relat
 ions crucial for program verification.\n\nThis talk presents our design an
 d implementation of coinductive predicates in Lean 4. Our approach leverag
 es lattice theory and the impredicativity of Lean's propositional universe
  to encode coinductive predicates and their proof principles directly with
 in Lean's existing type theory\, no kernel extensions required. Our implem
 entation supports mutual coinduction\, including mixed coinductive and ind
 uctive definitions. The talk will also touch on supporting syntax similar 
 to the one for usual inductive types and compiling such definitions to mon
 otone maps.\n\nJoint work with Joachim Breitner (Lean FRO\, Germany).\n
LOCATION:https://researchseminars.org/talk/LT2026/31/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Oliver Dressler
DTSTART:20260122T153000Z
DTEND:20260122T160000Z
DTSTAMP:20260419T233655Z
UID:LT2026/32
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/32/">
 lean-lsp-mcp: Tools for agentic interaction with Lean</a>\nby Oliver Dress
 ler as part of Lean Together 2026\n\n\nAbstract\nlean-lsp-mcp gives agents
  the same feedback that human users get from the IDE by exposing tools for
  querying the Lean language server and external search APIs. This talk giv
 es an overview\, presents use cases\, and discusses challenges when workin
 g with lean-lsp-mcp.\n
LOCATION:https://researchseminars.org/talk/LT2026/32/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260122T160000Z
DTEND:20260122T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/33
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/33/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/33/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hannah Scholz (University of Bonn)
DTSTART:20260122T163000Z
DTEND:20260122T170000Z
DTSTAMP:20260419T233655Z
UID:LT2026/34
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/34/">
 Formalisation of CW complexes</a>\nby Hannah Scholz (University of Bonn) a
 s part of Lean Together 2026\n\n\nAbstract\nCW complexes are a class of to
 pological spaces that are of particular importance in algebraic topology. 
 Intuitively\, they are the result of glueing continuous images of discs to
 gether along their boundaries. My talk will concern the classical way of d
 efining them\, close to Whitehead’s original definition. I will first di
 scuss the definition and a particular challenge with typeclass inference t
 hat we faced when implementing it in Lean. Afterwards\, I will report on t
 he current status of CW complexes in Lean and lastly\, I will give a glimp
 se of the mathematically most interesting part of the project: the product
  of CW complexes. All the work that I will be presenting was done together
  with and supervised by Prof. Floris van Doorn.\n
LOCATION:https://researchseminars.org/talk/LT2026/34/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Salvatore Mercuri (Imperial College London)
DTSTART:20260122T170000Z
DTEND:20260122T173000Z
DTSTAMP:20260419T233655Z
UID:LT2026/35
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/35/">
 A bottom-up approach to formalisation in the FLT project</a>\nby Salvatore
  Mercuri (Imperial College London) as part of Lean Together 2026\n\n\nAbst
 ract\nThis talk will describe a collaborative multi-author project to deve
 lop foundational material required for the formalisation of the proof of F
 ermat’s Last Theorem. The culmination of this project is a sorry-free pr
 oof that a certain space of automorphic cusp forms is finite-dimensional. 
 We will report on the overall status of this project\, with a particular f
 ocus on the adele ring sub-project\, as well as the ongoing efforts to ups
 tream our results to mathlib.\n
LOCATION:https://researchseminars.org/talk/LT2026/35/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Etienne Marion (École Normale Supérieure de Lyon)
DTSTART:20260122T173000Z
DTEND:20260122T180000Z
DTSTAMP:20260419T233655Z
UID:LT2026/36
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/36/">
 Formalization of the Ionescu-Tulcea theorem in Mathlib</a>\nby Etienne Mar
 ion (École Normale Supérieure de Lyon) as part of Lean Together 2026\n\n
 \nAbstract\nWe describe the formalization of the Ionescu-Tulcea theorem\, 
 showing the existence of a probability measure on the space of trajectorie
 s of a Markov chain\, in the proof assistant Lean using the integrated lib
 rary Mathlib. We first present Markov kernels\, which are the objects of i
 nterest in this theorem. Then after giving a glimpse of the proof\, we exp
 ose the difficulties which arise when trying to formalize it\, and how the
 y were overcome.\n
LOCATION:https://researchseminars.org/talk/LT2026/36/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Julius Marx (Hochschule RheinMain)
DTSTART:20260122T180000Z
DTEND:20260122T183000Z
DTSTAMP:20260419T233655Z
UID:LT2026/37
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/37/">
 MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL in Lean</a>
 \nby Julius Marx (Hochschule RheinMain) as part of Lean Together 2026\n\n\
 nAbstract\nThis talk introduces MRiscX\, a domain-specific language (DSL) 
 designed to lower the barrier to entry into the world of formal methods. E
 mbedded in Lean\, MRiscX allows RISC-V assembly code to be easily annotate
 d with formal specifications\, which can then be interactively verified. B
 y enabling the correctness of assembly code to be proven with minimal effo
 rt\, MRiscX makes it significantly easier for newcomers to get started wit
 h formal methods.\n
LOCATION:https://researchseminars.org/talk/LT2026/37/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Kim Morrison (Lean Focused Research Organization)
DTSTART:20260123T130000Z
DTEND:20260123T133000Z
DTSTAMP:20260419T233655Z
UID:LT2026/38
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/38/">
 grind</a>\nby Kim Morrison (Lean Focused Research Organization) as part of
  Lean Together 2026\n\n\nAbstract\nI'll give a quick introduction to Lean'
 s powerful new automation `grind`\, touching on library design\, theorem s
 earch\, diagnostics\, and custom grind tactics.\n
LOCATION:https://researchseminars.org/talk/LT2026/38/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Alex Best (Harmonic)
DTSTART:20260123T133000Z
DTEND:20260123T140000Z
DTSTAMP:20260419T233655Z
UID:LT2026/39
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/39/">
 Aristotle\, an AI theorem prover using Lean</a>\nby Alex Best (Harmonic) a
 s part of Lean Together 2026\n\n\nAbstract\nI'll describe the principles u
 nderlying the development of Aristotle\, an AI theorem prover trained via 
 reinforcement learning on Lean proofs. I'll give a demo of how this can be
  accessed and show some examples of projects making heavy use of this tech
 nology\, in particular those using it for novel mathematical proofs and fo
 r library development.\n
LOCATION:https://researchseminars.org/talk/LT2026/39/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Son Ho
DTSTART:20260123T153000Z
DTEND:20260123T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/40
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/40/">
 Formal Verification of Rust Cryptographic Code in Lean with Aeneas</a>\nby
  Son Ho as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/40/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260123T143000Z
DTEND:20260123T150000Z
DTSTAMP:20260419T233655Z
UID:LT2026/41
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/41/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/41/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Floris van Doorn
DTSTART:20260123T150000Z
DTEND:20260123T153000Z
DTSTAMP:20260419T233655Z
UID:LT2026/42
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/42/">
 Lessons from the Carleson project</a>\nby Floris van Doorn as part of Lean
  Together 2026\n\n\nAbstract\nFrom June 2024 to July 2025 the Carleson pro
 ject ran\, a community-driven collaboration to formalize a modern generali
 zation of Carleson's theorem\, proven by the Bonn harmonic analysis group 
 in 2023. In this talk I will reflect on the project\, discuss what lessons
  we can learn from it\, and describe further formalization goals in harmon
 ic analysis.\n
LOCATION:https://researchseminars.org/talk/LT2026/42/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Michal Mrugala (École normale supérieure de Lyon)
DTSTART:20260123T140000Z
DTEND:20260123T143000Z
DTSTAMP:20260419T233655Z
UID:LT2026/43
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/43/">
 Formalizing Class Field Theory</a>\nby Michal Mrugala (École normale sup
 érieure de Lyon) as part of Lean Together 2026\n\n\nAbstract\nClass field
  theory is one of the big achievements of twentieth-century number theory.
  This talk describes ongoing work to formalize class field theory in Lean\
 , with a focus on progress made during a CMI workshop in July 2025. I will
  also share reflections on the workshop from the perspective of a particip
 ant.\n
LOCATION:https://researchseminars.org/talk/LT2026/43/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Break
DTSTART:20260123T160000Z
DTEND:20260123T163000Z
DTSTAMP:20260419T233655Z
UID:LT2026/44
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/44/">
 Break</a>\nby Break as part of Lean Together 2026\n\nAbstract: TBA\n
LOCATION:https://researchseminars.org/talk/LT2026/44/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Joël Riou (Paris-Saclay University)
DTSTART:20260123T163000Z
DTEND:20260123T170000Z
DTSTAMP:20260419T233655Z
UID:LT2026/45
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/45/">
 Formalization of homotopy theory in Lean</a>\nby Joël Riou (Paris-Saclay 
 University) as part of Lean Together 2026\n\n\nAbstract\nModel categories 
 structures introduced by Quillen are a framework in order to do homotopy t
 heory. In this talk\, I will outline my formalization of the model categor
 y structures on the categories of topological spaces and simplicial sets.\
 n
LOCATION:https://researchseminars.org/talk/LT2026/45/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Atticus Kuhn (University of Cambridge\, Department of Computer Sci
 ence)
DTSTART:20260123T170000Z
DTEND:20260123T173000Z
DTSTAMP:20260419T233655Z
UID:LT2026/46
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/46/">
 Verification of model-checking techniques in Lean</a>\nby Atticus Kuhn (Un
 iversity of Cambridge\, Department of Computer Science) as part of Lean To
 gether 2026\n\n\nAbstract\nVardi proved that model-checking LTL properties
  can be witnessed by the existence of a certain ranking function. We have 
 formalised Vardi's result in Lean4 for both finite and infinite-state syst
 ems. Additionally\, we show how the Lean formalisation can be extended to 
 Neural Ranking Functions (NRFs)\, a modern technique that allows candidate
  ranking functions to be machine-generated.\n
LOCATION:https://researchseminars.org/talk/LT2026/46/
END:VEVENT
END:VCALENDAR