Skip to main content
Glama

Formath MCP

by yutayamamoto

Server Configuration

Describes the environment variables required to run the server.

NameRequiredDescriptionDefault

No arguments

Schema

Prompts

Interactive templates invoked by user choice

NameDescription

No prompts

Resources

Contextual data attached and managed by the client

NameDescription

No resources

Tools

Functions exposed to the LLM to take actions

NameDescription
ping

Health check tool returning a simple response.

scaffold_project

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_message

Return quick instructions for using this server in Cursor.

tex_extract

Extract definitions and lemmas from a TeX file. Returns a compact JSON summary.

formalize_tex

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.

render_entities_markdown

Regenerate formath/entities.md from formath/entities.jsonl for a project.

tasks_upsert

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_list

List tasks (optionally filter by state). Returns JSON list (latest per id).

tasks_transition

Append a state transition record for a task id.

progress_summary

Return a compact JSON summary of progress: entity counts and tasks by state.

render_checklist_markdown

Generate formath/checklist.md from tasks.jsonl (latest per id).

workflow_formalize_all

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_entities

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_next

Mark next open tasks as in_progress (up to limit). Returns transitioned ids.

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