これは、VSCode 用に設計された MCP サーバーで、Lean Mathlib 4 のドキュメントを検索するために特別に作成されています。ユーザーは宣言、モジュール、およびインスタンスを検索し、関連するドキュメントのリンクと詳細情報を取得できます。

LeanIX MCP統合プロジェクトは、LeanIXとAIアシスタントをつなぐMCPサーバーを提供し、5つのMCPツールを通じてLeanIXのGraphQL API機能を公開します。これには統計の表示、検索、サブスクリプション管理、データテーブルの作成と更新などの機能が含まれます。