lean-lsp-mcp

gemini_code_golf

Simplify Lean code with Google Gemini. Submit your Lean code and get a more concise version.

Instructions

This tool uses the Google Gemini model to simplify Lean code compiled by the compiler.

It uses Google's Gemini API to generate text responses. You need to set the GOOGLE_API_KEY environment variable.

Args:
    lean_code (str, optional): The lean code to be golfed.
    model (str, optional): The Gemini model to use. The default is "gemini-3-pro-preview".
    temperature (float, optional): The generated temperature, controlling randomness. The default is 0.7.

Returns:
    str: Gemini model response or error message

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "lean_code": "<lean_code>"
    },
    "name": "gemini_code_golf"
  }
}

Input Schema

Name	Required	Default
`model`	No	gemini-3-pro-preview
`lean_code`	Yes
`temperature`	No

Output Schema

Name	Required	Description	Default
`result`	Yes

Schema Changelog

Changes observed during successful MCP inspections.

First observedv0.14.1Aug 2, 2026

TDQS

C2.7/5.0

Behavior2/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Without annotations, the description carries the full burden, but it only discloses the API key requirement and the return type. It does not mention that code is sent to an external service, potential rate limits/costs, or what 'golfed' output looks like, leaving significant behavioral ambiguity.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness3/5

Is the description appropriately sized, front-loaded, and free of redundancy?

The description has a clear Args/Returns structure and is reasonably concise, but it repeats the Google/Gemini dependency in consecutive sentences and uses awkward phrasing. It would be tighter with the redundancy removed.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness3/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

The description covers the essential parameters, return type, and the prerequisite, but misses important context such as the meaning of 'golfed,' whether the code is transformed in place, and external API implications. It is adequate but not complete for an external-call tool.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters2/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

The description lists all three parameters with meanings and defaults, compensating for the schema's 0% description coverage. However, it erroneously marks lean_code as 'optional' while the schema marks it as required, which is a dangerous contradiction that could mislead an agent into omitting a required argument.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description clearly states the tool 'uses the Google Gemini model to simplify Lean code,' distinguishing it from sibling tools that inspect or interact with Lean files. However, the phrase 'compiled by the compiler' is confusing and it doesn't explicitly contrast with the other Gemini-based tools.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines2/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

No guidance is provided on when to choose this tool over alternatives such as gemini_informal_prover or discussion_partner. The only usage hint is the GOOGLE_API_KEY prerequisite, which is operational, not selectional.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.