prove_lean_file
Submit a Lean file to automatically fill in 'sorry' placeholders and generate proofs using the Aristotle theorem prover.
Instructions
Submits a local Lean file to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |
Implementation Reference
- main.py:14-38 (handler)The handler function for the 'prove_lean_file' MCP tool, including registration via @mcp.tool(). It validates the Lean file path, submits it to Aristotle for proving 'sorry' placeholders using Project.prove_from_file, monitors the project, and returns the project ID.
@mcp.tool() async def prove_lean_file( file_path: str, ctx: Context | None = None, ) -> str: """ Submits a local Lean file to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately. """ path = Path(file_path) if not path.exists(): raise FileNotFoundError(f"File not found: {file_path}") if ctx: await ctx.info(f"Submitting {file_path} to Aristotle...") project_id = await Project.prove_from_file( # type: ignore input_file_path=path, project_input_type=ProjectInputType.FORMAL_LEAN, wait_for_completion=False ) monitored_projects.add(project_id) return f"Project started with ID: {project_id}."