prove_lean_code
Submit Lean code to automatically fill 'sorry' placeholders and generate proofs using the Aristotle theorem proving API.
Instructions
Submits Lean code directly to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| lean_code | Yes |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |
Implementation Reference
- main.py:127-145 (handler)The main handler function for the 'prove_lean_code' tool. It is registered via the @mcp.tool() decorator. This function takes Lean code as a string, submits it to Aristotle's Project.prove_from_file for proving (filling 'sorry' placeholders), adds the project to monitored_projects, and returns the project ID.
async def prove_lean_code( lean_code: str, ctx: Context | None = None, ) -> str: """ Submits Lean code directly to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately. """ if ctx: await ctx.info("Submitting Lean code to Aristotle...") project_id = await Project.prove_from_file( # type: ignore input_content=lean_code, project_input_type=ProjectInputType.FORMAL_LEAN, wait_for_completion=False ) monitored_projects.add(project_id) return f"Project started with ID: {project_id}."