[philipp-gayret]

Maybe https://context7.com/leanprover/lean4 is what you're looking for? I am not familiar with Lean 4 but Context7 has been working well enough for me, working in a completely different field though.

For OP: Zig is also on Context7.

[afirium]

LLMs have issues with zig, namely outdated docs. Then I found @jedisct1's project, context7 MCPwhich provides a way to search through zig docs using natural language: https://github.com/jedisct1/zig-for-mcp

But context7 returns semantically processed responses that often summarize or rephrase the information instead of quoting it. And that's why there is now zig-mcp which returns documentation in markdown format for stdlib and builtin functions

[Syzygies]

Thanks! Great idea, I'm not sure why it doesn't actually work better for Lean.