Aristotle MCP Server

Instructions

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}."