prove_informal_text
Formalizes and proves mathematical statements expressed in natural language using the Aristotle API, returning a Project ID for tracking.
Instructions
Submits natural language mathematics directly to be formalized and proved. Returns the Project ID immediately.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| text | Yes | ||
| formal_context_path | No |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |
Implementation Reference
- main.py:147-168 (handler)The handler function for the 'prove_informal_text' tool. It is decorated with @mcp.tool(), which registers it as an MCP tool. The function submits informal text to Aristotle via Project.prove_from_file and returns the project ID.
@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}."