3 ms·
Maybe 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 bee
by philipp-gayret 1y ago
Maybe 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.