Formath MCP
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Capabilities
Server capabilities have not been inspected yet.
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| pingA | Health check tool returning a simple response. |
| scaffold_projectA | Create a minimal formalization project layout with TeX, rules, and placeholders. Args: project_name: Name of the project directory to create base_dir: Optional base directory. If omitted, creates under repo-local "projects/". |
| quickstart_messageB | Return quick instructions for using this server in Cursor. |
| tex_extractB | Extract definitions and lemmas from a TeX file. Returns a compact JSON summary. |
| formalize_texB | End-to-end minimal pipeline: TeX -> Formath JSONL -> Lean stub module. Writes to sibling directories beside the TeX's |
| render_entities_markdownC | Regenerate formath/entities.md from formath/entities.jsonl for a project. |
| tasks_upsertB | Create or update a task. Returns the task id. Task shape (flexible): { id?, title, kind?, state?, entity_id?, priority?, assignee? } States: open|in_progress|blocked|done |
| tasks_listC | List tasks (optionally filter by state). Returns JSON list (latest per id). |
| tasks_transitionC | Append a state transition record for a task id. |
| progress_summaryB | Return a compact JSON summary of progress: entity counts and tasks by state. |
| render_checklist_markdownB | Generate formath/checklist.md from tasks.jsonl (latest per id). |
| workflow_formalize_allA | Formalize all *.tex under <project_root>/tex. naming: "by_file" → module name from file stem (capitalized), otherwise use "Main". Returns a JSON array of results per file. |
| tasks_autogen_from_entitiesB | Create open tasks for entities of given kind that do not already have tasks. Default kind is 'fact' (lemmas). Returns number of tasks created. |
| tasks_pick_nextB | Mark next open tasks as in_progress (up to limit). Returns transitioned ids. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
Latest Blog Posts
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