Aristotle MCP Server

Instructions

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