lean-lsp-mcp: Tools for agentic interaction with Lean
Oliver Dressler
Thu Jan 22, 15:30-16:00 (4 weeks ago)
Abstract: lean-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 gives an overview, presents use cases, and discusses challenges when working with lean-lsp-mcp.
logic in computer sciencemathematical softwareMathematics
Audience: researchers in the discipline
| Organizer: | Jireh Loreaux* |
| *contact for this listing |
Export talk to