Formath MCP
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
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 /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 | |
TDQS
Scored across 14 tools
Most tools have distinct purposes, such as tex_extract for parsing TeX, tasks_* for task management, and render_* for documentation generation. However, there is some potential overlap between tasks_autogen_from_entities and tasks_upsert, as both involve task creation, which could cause minor confusion in selection.
Tool names follow a highly consistent snake_case pattern with clear verb_noun structures, such as tasks_list, tasks_upsert, render_entities_markdown, and tex_extract. All tools adhere to this convention, making the set predictable and easy to navigate.
With 14 tools, the server is well-scoped for its formalization project management domain. The tools cover essential areas like TeX processing, task management, project scaffolding, and progress tracking, with each tool serving a clear and necessary function.
The tool set provides comprehensive coverage for formalization workflows, including extraction, task lifecycle management, and documentation. A minor gap exists in direct entity manipulation tools, such as updating or deleting entities, but agents can work around this using existing tools like tasks_upsert and render_entities_markdown.