BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Oliver Dressler
DTSTART:20260122T153000Z
DTEND:20260122T160000Z
DTSTAMP:20260420T025016Z
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
END:VCALENDAR