Loading ToolBench
MCP server for automated Lean 4 proof annotations (Aesop / Grind)
The server has 9 tools with generally good naming (verb-noun pattern) and comprehensive input schemas, but critical gaps in parameter descriptions, output schema documentation, and error handling guidance. Tool descriptions vary widely in quality (some detailed, some minimal). Schema definitions are present but lack critical documentation for LLM consumption. No evidence of error classification or recovery guidance. The domain (Lean proof automation) is specialized and well-scoped, but definition patterns fall short of production grade.
Get proof context for a theorem.
Run single-theorem automation probe with deterministic classification. Measures what happens when automation (aesop, aesop?, or grind) is applied to a single theorem under controlled conditions. Returns structured outcome with classification (trivial, promising, failed, timed_out).
Run batch automation probing across multiple theorems in a file. Produces a heatmap of automation behavior for triage and prioritization. Runs probe on each theorem with fixed parameters and aggregates results into summary statistics.
Rank theorem automation targets in a Lean file by objective.
Scan a Lean file and return summary information about theorems.
Analyze a single theorem in a Lean file with detailed structure and automation.
Two tools (try_automated_proof, get_proof_context) have minimal or no descriptions and no visible input schema definitions. These violate the critical pattern that every tool must have a non-empty description and formal input schema.
No output schemas are documented for any tool. LLMs need to know what fields to expect in responses to plan downstream calls and extract the right data. Production tools document return types explicitly.
No error handling or recovery guidance in any tool description. Tools that run external processes (verify, probe, probe_file) need to specify timeout behavior, retryability, and what to do when automation fails.
Inferred effective spec: <=2025-11-25.
| Scored | Grade | Overall | Spec posture | Rubric |
|---|---|---|---|---|
| 2026-09-23 | D | 57 | <=2025-11-25 | v2 |
Search for automated proof with rich feedback and LLM-controlled parameters. Enhanced search tool with LLM-controlled search depth presets, rich feedback mechanisms, and support for all candidate sources including original_proof_refs.
Try automated proof with a specific hint set.
Verify a Lean file or theorem with deterministic, sandboxed execution.
Parameter descriptions are inconsistent and sometimes missing semantic detail. For example, 'trace_config' in probe is described as 'Optional trace configuration dict' with no explanation of what trace options are valid or what effects they have.
Some parameters with constrained values are not documented as enums. For example, 'mode' in probe accepts 'aesop', 'aesop?', or 'grind', and 'search_depth' in search_automated_proof accepts 'quick', 'normal', 'deep', 'exhaustive', these should be declared as enum constraints rather than free-form strings.
No guidance on when to use similar tools. For example, probe vs probe_file, or rank_targets vs search_automated_proof, descriptions do not clearly explain when an LLM should select one over the other.
Time budget parameters (budget_s, budget_s_per, search_budget_s) lack explicit minimum/maximum constraints and guidance on reasonable values. The description suggests 'minimum recommended: 30.0 for Mathlib' but does not make it a formal constraint.