Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Schema
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| 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 |
| 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. |