Formath MCP

formalize_tex

Converts TeX documents into Lean code via Formath JSONL, generating entities.jsonl and lean/src/<module>.lean files in sibling directories. Streamlines mathematical formalization workflows.

Instructions

End-to-end minimal pipeline: TeX -> Formath JSONL -> Lean stub module.

Writes to sibling directories beside the TeX's tex/ folder: formath/entities.jsonl and lean/src/<module>.lean.

Input Schema

Name	Required	Description	Default
`module_name`	No		Main
`tex_path`	Yes

Input Schema (JSON Schema)

{
  "properties": {
    "module_name": {
      "default": "Main",
      "title": "Module Name",
      "type": "string"
    },
    "tex_path": {
      "title": "Tex Path",
      "type": "string"
    }
  },
  "required": [
    "tex_path"
  ],
  "title": "formalize_texArguments",
  "type": "object"
}

Install Server

HTTP connection URL

Other Tools from Formath MCP

Related Tools

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/yutayamamoto/formath-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server