I need a version of this for Lean 4; perhaps I can adapt this code.

AI generally struggles with less popular languages, and particularly with Lean 4, which is an excellent general purpose programming language that happens to have a primary goal to be a proof assistant. This skew in the training corpus really confuses AI.

Claude Opus 4 does better. I've looked at ways to serve the Lean 4 documentation; this Zig project is a better model for me.

Nia (https://www.trynia.ai) should generalize these tools, but it appears to have a "code base" focus for now. The right approach, but too specific a "system prompt".

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.

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

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

I have a gut feeling that writing this kind of MCP server can't be the future of software development. I'd expect a two year old AI model to need this kind of handholding, but I don't understand why it's still necessary.

Couldn't any modern AI model know that Zig docs are relevant to the question, figure out how to find the docs, write some code to parse it, and guess how frequently to update it's cache?

I expect there to be plenty of problems AI can't write for the foreseeable future but they have a very different vibe from this.

Edit: I just asked Claude Sonnet 4 to pretend it has a tool that makes docs available that has an update frequency parameter. It said the zig stdlib should be updated weekly but the Java stdlib would only need quarterly. Seems reasonable to me.

That's exactly what zig-mcp does. It gives the LLM tools like search_std_lib, get_std_lib_item, and it decides when and how to use them based on context

Stop thinking of models as all-knowing oracles; they aren't and shouldn't be. They are reasoning engines. You will always need to provide relevant and up to date context for them to work with as ground level truth, and the quality of your results will be a function of the density and quality of that context, just as a human developer is far more effective with access to web search and documentation.

> outdated docs are a problem

What do you need (external) docs for? Stdlib source code is available right away.

Are there any MCP servers that enrich the context with data from a language server and fetches relevant documentation based on the types provided from that information?