Health check tool returning a simple response.

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/".

Return quick instructions for using this server in Cursor.

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

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.

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

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

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

Append a state transition record for a task id.

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

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

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.

Create open tasks for entities of given kind that do not already have tasks.

Default kind is 'fact' (lemmas). Returns number of tasks created.

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