prove_informal
Formalizes and proves mathematical statements from natural language files using Lean theorem proving, returning a Project ID for tracking.
Instructions
Submits a file containing natural language mathematics (Text, Markdown, LaTeX) to be formalised and proved. Returns the Project ID immediately.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | ||
| formal_context_path | No |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |
Implementation Reference
- main.py:39-64 (handler)The handler function for the 'prove_informal' tool. It is registered via the @mcp.tool() decorator and handles submitting an informal mathematics file to Aristotle for formalization and proof using Project.prove_from_file, returning the project ID.
@mcp.tool() async def prove_informal( file_path: str, formal_context_path: Optional[str] = None, ctx: Context | None = None, ) -> str: """ Submits a file containing natural language mathematics (Text, Markdown, LaTeX) to be formalised and proved. 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 informal file {file_path} to Aristotle...") project_id = await Project.prove_from_file( # type: ignore input_file_path=path, project_input_type=ProjectInputType.INFORMAL, formal_input_context=formal_context_path, wait_for_completion=False ) monitored_projects.add(project_id) return f"Project started with ID: {project_id}." - main.py:147-168 (handler)A related handler for submitting informal text directly (without file), similar to prove_informal.
@mcp.tool() async def prove_informal_text( text: str, formal_context_path: Optional[str] = None, ctx: Context | None = None, ) -> str: """ Submits natural language mathematics directly to be formalized and proved. Returns the Project ID immediately. """ if ctx: await ctx.info("Submitting informal text to Aristotle...") project_id = await Project.prove_from_file( # type: ignore input_content=text, project_input_type=ProjectInputType.INFORMAL, formal_input_context=formal_context_path, wait_for_completion=False ) monitored_projects.add(project_id) return f"Project started with ID: {project_id}."