MCP Tools Reference

tools

Defines MCP tools for interacting with the Lean Explore search engine.

These tools provide functionalities such as searching for statement groups, retrieving specific groups by ID, and getting their dependencies. They utilize a backend service (either an API client or a local service) made available through the MCP application context.

Classes

Functions

get_by_id async

get_by_id(ctx, group_id)

Retrieves specific statement groups by their unique identifier(s).

The display_statement_text field is omitted from the response. This tool always returns a list of results.

Parameters:

Name	Type	Description	Default
ctx	Context	The MCP context, providing access to the backend service.	required
group_id	Union[int, List[int]]	A single unique integer identifier or a list of identifiers of the statement group(s) to retrieve. For example, 12345 or [12345, 67890].	required

Returns:

Type	Description
List[Optional[Dict[str, Any]]]	A list of dictionaries, where each dictionary corresponds to the
List[Optional[Dict[str, Any]]]	APISearchResultItem model. If an ID is not found, its corresponding
List[Optional[Dict[str, Any]]]	entry in the list will be None (serialized as JSON null by MCP).

Source code in src/lean_explore/mcp/tools.py

@mcp_app.tool()
async def get_by_id(
    ctx: MCPContext, group_id: Union[int, List[int]]
) -> List[Optional[Dict[str, Any]]]:
    """Retrieves specific statement groups by their unique identifier(s).

    The `display_statement_text` field is omitted from the response. This tool
    always returns a list of results.

    Args:
        ctx: The MCP context, providing access to the backend service.
        group_id: A single unique integer identifier or a list of identifiers
                  of the statement group(s) to retrieve. For example, `12345` or
                  `[12345, 67890]`.

    Returns:
        A list of dictionaries, where each dictionary corresponds to the
        APISearchResultItem model. If an ID is not found, its corresponding
        entry in the list will be None (serialized as JSON null by MCP).
    """
    backend = await _get_backend_from_context(ctx)
    logger.info(f"MCP Tool 'get_by_id' called for group_id(s): {group_id}")

    backend_items: Union[
        Optional[APISearchResultItem], List[Optional[APISearchResultItem]]
    ]
    if asyncio.iscoroutinefunction(backend.get_by_id):
        backend_items = await backend.get_by_id(group_id=group_id)
    else:
        backend_items = backend.get_by_id(group_id=group_id)

    # Normalize to a list for consistent return type
    items_list = (
        [backend_items] if not isinstance(backend_items, list) else backend_items
    )

    mcp_items = []
    for item in items_list:
        if item:
            mcp_item = _prepare_mcp_result_item(item)
            mcp_items.append(mcp_item.model_dump(exclude_none=True))
        else:
            mcp_items.append(None)

    return mcp_items

get_dependencies async

get_dependencies(ctx, group_id)

Retrieves direct dependencies (citations) for specific statement group(s).

The display_statement_text field within each cited item is omitted from the response. This tool always returns a list of results.

Parameters:

Name	Type	Description	Default
ctx	Context	The MCP context, providing access to the backend service.	required
group_id	Union[int, List[int]]	A single unique integer identifier or a list of identifiers for the statement group(s) for which to fetch direct dependencies. For example, 12345 or [12345, 67890].	required

Returns:

Type	Description
List[Optional[Dict[str, Any]]]	A list of dictionaries, where each dictionary corresponds to the
List[Optional[Dict[str, Any]]]	APICitationsResponse model. If a source group ID is not found or has
List[Optional[Dict[str, Any]]]	no dependencies, its corresponding entry will be None.

Source code in src/lean_explore/mcp/tools.py

@mcp_app.tool()
async def get_dependencies(
    ctx: MCPContext, group_id: Union[int, List[int]]
) -> List[Optional[Dict[str, Any]]]:
    """Retrieves direct dependencies (citations) for specific statement group(s).

    The `display_statement_text` field within each cited item is omitted
    from the response. This tool always returns a list of results.

    Args:
        ctx: The MCP context, providing access to the backend service.
        group_id: A single unique integer identifier or a list of identifiers for
                  the statement group(s) for which to fetch direct dependencies.
                  For example, `12345` or `[12345, 67890]`.

    Returns:
        A list of dictionaries, where each dictionary corresponds to the
        APICitationsResponse model. If a source group ID is not found or has
        no dependencies, its corresponding entry will be None.
    """
    backend = await _get_backend_from_context(ctx)
    logger.info(f"MCP Tool 'get_dependencies' called for group_id(s): {group_id}")

    backend_responses: Union[
        Optional[APICitationsResponse], List[Optional[APICitationsResponse]]
    ]
    if asyncio.iscoroutinefunction(backend.get_dependencies):
        backend_responses = await backend.get_dependencies(group_id=group_id)
    else:
        backend_responses = backend.get_dependencies(group_id=group_id)

    # Normalize to a list for consistent return type
    responses_list = (
        [backend_responses]
        if not isinstance(backend_responses, list)
        else backend_responses
    )
    final_mcp_responses = []

    for response in responses_list:
        if response:
            mcp_citations_list = []
            for backend_item in response.citations:
                mcp_citations_list.append(_prepare_mcp_result_item(backend_item))

            final_response = APICitationsResponse(
                source_group_id=response.source_group_id,
                citations=mcp_citations_list,
                count=len(mcp_citations_list),
            )
            final_mcp_responses.append(final_response.model_dump(exclude_none=True))
        else:
            final_mcp_responses.append(None)

    return final_mcp_responses

search async

search(ctx, query, package_filters=None, limit=10)

Searches Lean statement groups by a query string or list of strings.

This tool allows for filtering by package names and limits the number of results returned per query.

Parameters:

Name	Type	Description	Default
ctx	Context	The MCP context, providing access to shared resources like the backend service.	required
query	Union[str, List[str]]	A single search query string or a list of query strings. For example, "continuous function" or ["prime number theorem", "fundamental theorem of arithmetic"].	required
package_filters	Optional[List[str]]	An optional list of package names to filter the search results by. For example, ["Mathlib.Analysis", "Mathlib.Order"]. If None or empty, no package filter is applied.	None
limit	int	The maximum number of search results to return per query. Defaults to 10. Must be a positive integer.	10

Returns:

Type	Description
List[Dict[str, Any]]	A list of dictionaries, where each dictionary corresponds to the
List[Dict[str, Any]]	APISearchResponse model. Each response contains the search results
List[Dict[str, Any]]	for a single query. The display_statement_text field within each
List[Dict[str, Any]]	result item is omitted.

Source code in src/lean_explore/mcp/tools.py

@mcp_app.tool()
async def search(
    ctx: MCPContext,
    query: Union[str, List[str]],
    package_filters: Optional[List[str]] = None,
    limit: int = 10,
) -> List[Dict[str, Any]]:
    """Searches Lean statement groups by a query string or list of strings.

    This tool allows for filtering by package names and limits the number
    of results returned per query.

    Args:
        ctx: The MCP context, providing access to shared resources like the
             backend service.
        query: A single search query string or a list of query strings. For
               example, "continuous function" or ["prime number theorem",
               "fundamental theorem of arithmetic"].
        package_filters: An optional list of package names to filter the search
                         results by. For example, `["Mathlib.Analysis",
                         "Mathlib.Order"]`. If None or empty, no package filter
                         is applied.
        limit: The maximum number of search results to return per query.
               Defaults to 10. Must be a positive integer.

    Returns:
        A list of dictionaries, where each dictionary corresponds to the
        APISearchResponse model. Each response contains the search results
        for a single query. The `display_statement_text` field within each
        result item is omitted.
    """
    backend = await _get_backend_from_context(ctx)
    logger.info(
        f"MCP Tool 'search' called with query/queries: '{query}', "
        f"packages: {package_filters}, tool_limit: {limit}"
    )

    if not hasattr(backend, "search"):
        logger.error("Backend service does not have a 'search' method.")
        raise RuntimeError("Search functionality not available on configured backend.")

    tool_limit = max(1, limit)
    backend_responses: Union[APISearchResponse, List[APISearchResponse]]

    # Conditionally await based on the backend's search method type
    if asyncio.iscoroutinefunction(backend.search):
        backend_responses = await backend.search(
            query=query, package_filters=package_filters
        )
    else:
        backend_responses = backend.search(query=query, package_filters=package_filters)

    # Normalize to a list for consistent processing, handling None from backend.
    if backend_responses is None:
        responses_list = []
    else:
        responses_list = (
            [backend_responses]
            if isinstance(backend_responses, APISearchResponse)
            else backend_responses
        )

    final_mcp_responses = []

    for response_pydantic in responses_list:
        if not response_pydantic:
            logger.warning("A backend search returned None; skipping this response.")
            continue

        actual_backend_results = response_pydantic.results
        mcp_results_list = []
        for backend_item in actual_backend_results[:tool_limit]:
            mcp_results_list.append(_prepare_mcp_result_item(backend_item))

        final_mcp_response = APISearchResponse(
            query=response_pydantic.query,
            packages_applied=response_pydantic.packages_applied,
            results=mcp_results_list,
            count=len(mcp_results_list),
            total_candidates_considered=response_pydantic.total_candidates_considered,
            processing_time_ms=response_pydantic.processing_time_ms,
        )
        final_mcp_responses.append(final_mcp_response.model_dump(exclude_none=True))

    return final_mcp_responses