# Tools

> Every listed resource, editors’ picks first. The filters below can be combined.

- Search: append `?q=<keywords>` to the URL. Separate several keywords with spaces; all of them must match. Matches name, repository, tags, professions, description and README.
- Filter by type: append `?type=<cli|skill|plugin|mcp>` to the URL.
- Filter by profession: append `?profession=<profession id>` to the URL. Separate several ids with commas; a resource matches when it suits any of them. Ids are listed at https://hebbmind.com/api/v1/professions
- Filter by tag: append `?tag=<tag>` to the URL. Separate several tags with commas; a resource must carry all of them. Tags are listed at https://hebbmind.com/api/v1/tags

Tagged `lean`: 3 items.

- [lean-lsp-mcp](https://hebbmind.com/de/mcp/lean-lsp-mcp.md): [MCP] MCP server for the Lean 4 theorem prover: lets agents read proof goals, diagnostics and definitions and search theorems via LeanSearch and Loogle, helping mathematicians and students with formal proofs. Needs uv and the Lean toolchain; run it from the Lean project root.
- [Lean 4 Skills](https://hebbmind.com/de/plugin/lean4-skills.md): [Plugin] Lean 4 theorem-proving plugin with workflows to draft, formalize, prove, disprove, review and golf proofs, plus mathlib search, axiom checks and safety guardrails, helping mathematicians and teachers produce machine-checked proofs. Needs Lean 4 and mathlib; pairs well with lean-lsp-mcp.
- [QuantConnect Lean CLI](https://hebbmind.com/de/cli/lean-cli.md): [CLI] QuantConnect's official CLI drives the open-source LEAN engine locally or in the cloud to download data, backtest and optimize quant strategies and deploy them live. Requires a paid-tier QuantConnect organization; strategies in Python or C#; local runs need Docker. Get expert review.