4 ms·
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
by Syzygies 1y ago
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 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".
- philipp-gayret 1y agoMaybe https://context7.com/leanprover/lean4 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 1y agoLLMs 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 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 1y agoThanks! Great idea, I'm not sure why it doesn't actually work better for Lean.