Formath MCP
Extracts mathematical definitions, theorems, and proofs from TeX/LaTeX documents and converts them into structured intermediate representations for formal verification
Generates human-readable Markdown reports for entities, progress summaries, and task checklists from the mathematical formalization pipeline
Provides full-text search capabilities over mathematical entities and definitions stored in the system's knowledge base
Click on "Install Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type
@followed by the MCP server name and your instructions, e.g., "@Formath MCPformalize the TeX paper at projects/demo/tex/theorem.tex as module Theorem"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
Overview of Formath
Related MCP server: Fetch MCP Server
Minimal MCP quickstart
Install deps:
uv syncRun server:
uv run main.pyIn Cursor, register the MCP server, then try tools:
formath-mcp.ping()formath-mcp.scaffold_project(project_name="demo")
I/O ポリシー(最小)
tex/: 読み取り専用(参照のみ)
formath/*.jsonl: MCP ツール経由で read/write(履歴と一貫性のため)
formath/*.md: MCP ツールが *.jsonl から再生成(手動編集しない)
lean/: エージェントが read/write 可。自動生成・射影などパイプライン起因の書き込みは MCP(例:
formalize_tex)経由を推奨。手作業の証明編集は IDE から直接で OK。
エージェント行動シナリオ(最小例)
目的:
projects/demo1/tex/paper2.texを Lean 雛形に落とす(検証用の最小フロー)前提: Cursor に
formath-mcpを登録済み、サーバーが起動済み手順:
ヘルスチェック:
formath-mcp.ping()→ "pong"抽出(件数と概要を把握):
formath-mcp.tex_extract("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper2.tex")返り値に
definitions/lemmasの件数とサンプルを含む JSON が返る
形式化(最小雛形生成):
formath-mcp.formalize_tex("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper2.tex", module_name="Paper2")出力:
projects/demo1/formath/entities.jsonlに抽出エンティティを追記projects/demo1/lean/src/Paper2.leanを生成(Lean 安全な識別子に自動変換)
IDE で
Paper2.leanを開いて雛形を確認(必要に応じて LSP/ビルドで診断)参考:
paper.texにも同様に実行可能formath-mcp.formalize_tex("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper.tex", module_name="Paper")
メモ
本フローは「MCP ツールの形」を示す最小例です。型付け・import 推定・証明補助などは段階的に拡張予定です。
entities.jsonlにはテキスト出所(source.file/label)を記録します。ID/Lean 名はラベルから Lean 安全に変換されます。
MCP ツール一覧(現状の最小セット)
基本
ping()scaffold_project(project_name?, base_dir?)quickstart_message()
TeX → Formath → Lean
tex_extract(tex_path: str)formalize_tex(tex_path: str, module_name: str = "Main")render_entities_markdown(project_root?)
進捗/タスク
tasks_upsert(task: dict, project_root?)tasks_list(state?, project_root?)tasks_transition(task_id, state, project_root?)progress_summary(project_root?)render_checklist_markdown(project_root?)
使い方例(projects/demo1 を対象)
# 1) 抽出
formath-mcp.tex_extract("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper2.tex")
# 2) 形式化(Lean 雛形生成 + entities.jsonl 追記 + entities.md 再生成)
formath-mcp.formalize_tex("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper2.tex", module_name="Paper2")
# 3) 途中経過の人間可読ビュー(再生成)
formath-mcp.render_entities_markdown("/Users/yutayamamoto/repo/formath-mcp/projects/demo1")
# 4) タスク運用(最小)
formath-mcp.tasks_upsert({"title":"Formalize paper2","state":"in_progress","entity_id":"fact:lem:affine"}, \
"/Users/yutayamamoto/repo/formath-mcp/projects/demo1")
formath-mcp.progress_summary("/Users/yutayamamoto/repo/formath-mcp/projects/demo1")
formath-mcp.render_checklist_markdown("/Users/yutayamamoto/repo/formath-mcp/projects/demo1")進捗管理と途中再開の指針
人間可読ビュー
formath/entities.md: エンティティ一覧(TeX/Lean/Markdown アンカー付き、スニペット同梱)formath/checklist.md: タスク一覧(Open/In Progress/Blocked/Done)
途中再開
中断時は
tasks_listまたはchecklist.mdを確認し、対象タスクのentity_id(例:fact:lem:affine)に紐づけて再開実行後に
tasks_transition(task_id, "done")等で状態遷移、render_checklist_markdownで反映
計測/俯瞰
progress_summaryで種別別エンティティ数と状態別タスク数を把握
目的と設計原則
目的と設計原則 • 目的: TeX 論文から抽出した数学的内容を、LLM/エージェントが 一貫性ある中間表現(Formath) に整理し、Lean コードへ段階的に落とし込む。 • 原則
人手最小・再開容易(途中停止/再開・差分実行・履歴管理)
Lean 忠実(型・文脈・インスタンス・記法を明示)
出所管理(TeX の箇所へのアンカーと生成/検証の由来)
段階分離(NL→Formath→Lean を明確に分離)
グラフ構造(概念間依存関係・仮定コンテキストを明示)
⸻
コア・データモデル(エンティティ)
コア・データモデル(エンティティ)
Formath は JSONL(1 行 1 エンティティ) を基本とし、内部的にはグラフ(DAG)として扱います。すべてのエンティティは以下の共通フィールドを持ちます。 • id(安定 ID、ULID/UUID)、kind(“concept” | “definition” | “fact” | “theorem” | …) • title(人間可読名)、status(“draft” | “checked” | “rejected”) • source(TeX アンカー: ファイル名/行範囲/label)、provenance(作成者/ツール/時刻/信頼度) • deps(依存エンティティ ID 配列) • notes(任意メモ)
1.1 Concept(概念) • symbols: 使用する記号(name, latex, role: "const"|"pred"|"func", arity) • intended_sort: Lean 側の型(例 "Nat" | "ℝ" | "Group") • canonical_definition: Definition への参照(definition_id) • examples: 例示(term_text と必要なら lean_term)
1.2 Definition(定義) • concept_id • nl: 自然言語定義(最短・厳密) • iff_characterization: 主要同値(オプション) • guard_conditions: ドメイン制約(例: n ≥ 0) • lean_signature: name, params(束縛変数・型), returns(型), typeclass_params • lean_stub: 生成される Lean 定義の雛形(sorry 可) • tests: 例から誘導される Quick checks(LLM/Lean での小検証)
1.3 Fact(命題の最小単位) • context: 仮定リスト(束縛と型、型クラス要求) • statement: • nl: NL 命題 • semi_formal: 中間形式(例: プレディケート形式や簡易 AST) • lean_type: 期待される Lean の式(Prop) • justification: 参照(定理/定義/計算)とタクティク計画(ProofPlan 参照) • classification: "lemma"|"theorem"|"corollary"|"proposition"|… • lean_artifact: 生成された Lean コードスニペット(sorry あり可)、lsp_diagnostics
Theorem/Lemma/Corollary は Fact の classification で区別(別型にしない簡素設計)。
1.4 ProofPlan / ProofStep(証明計画) • goal_fact_id • strategy: "calc"|"by_cases"|"induction"|"contradiction"|… • steps: • kind: "apply"|"have"|"calc"|"rewrite"|… • target_subgoal(どのゴールに作用するか) • tactic_hint(simp [hoge], ring, …) • references(使う定理 ID / Lean 名) • resulting_goals(lean-lsp 実行後のゴールスナップショット)
1.5 Notation / Instance / Structure(Lean 依存成分) • Notation: 記法衝突・優先度、lean_notation、依存するスコープ • Instance: typeclass インスタンスの存在を明示(Mul α, TopologicalSpace X など) • Structure: 新規構造体/クラスの定義情報
1.6 MappingToLean(射影レイヤ) • targets: 生成/更新する Lean ファイル/モジュール • name_hints: Lean 名前付け指針(CamelCase/名前空間) • imports: 必要な import 一覧(Mathlib.*) • coercions: 既知の coercion/simp 設定
1.7 Task / TODO(進捗管理) • kind: "extract"|"disambiguate"|"stub"|"prove"|"refactor"|"lint" • entity_id / batch(論文節単位) • priority, assignee, due, state(open|in_progress|blocked|done) • blockers: 依存タスク/不足定義
⸻
「hoge number」例(最小 MVP 表現)
「hoge number」例(最小 MVP 表現)
{"id":"concept:hoge-number","kind":"concept","title":"hoge number", "symbols":[{"name":"Hoge","latex":"\mathrm{Hoge}","role":"pred","arity":1}], "intended_sort":"Nat","canonical_definition":"def:hoge-number","examples":[ {"term_text":"11"},{"term_text":"12"},{"term_text":"13"}], "source":{"file":"paper.tex","span":"L120-160","label":"def:hoge"}}
{"id":"def:hoge-number","kind":"definition","title":"def of hoge number", "concept_id":"concept:hoge-number", "nl":"A natural number is hoge iff it is > 10 and prime.", "iff_characterization":["∀ n, Hoge n ↔ (n > 10 ∧ Prime n)"], "lean_signature":{"name":"Hoge","params":[["n","Nat"]],"returns":"Prop"}, "lean_stub":"def Hoge (n : Nat) : Prop := n > 10 ∧ Nat.Prime n", "tests":[{"lean":"example : Hoge 11 := by decide? -- or: by decide"}], "source":{"file":"paper.tex","span":"L120-160"}}
{"id":"fact:hoge-odd","kind":"fact","title":"hoge numbers are odd", "context":[["n","Nat","Hoge n"]], "statement":{"nl":"If n is hoge then n is odd.", "semi_formal":"∀ n, Hoge n → Odd n","lean_type":"∀ n, Hoge n → Odd n"}, "classification":"lemma", "justification":{"strategy":"by_cases/prime→odd", "references":["Nat.Prime.odd"]}, "lean_artifact":"lemma hoge_odd : ∀ n, Hoge n → Odd n := by\n intro n h; exact (Nat.Prime.odd ?p)\n -- fill ?p from h\n sorry", "source":{"file":"paper.tex","span":"L161-185"}}
ポイント • 「properties 配列を文字列で並べる」よりも、Fact として正規化すると依存や証明計画が扱いやすい。 • Definition で lean_stub を持ち、Fact の lean_artifact と分離。
⸻
アクセス(MCP 経由の操作)
アクセス(MCP 経由の操作)
serena(ファイル IO)、lean-lsp(型チェック/ゴール取得)、独自 MCP formath を想定。
3.1 formath MCP(例) • formath.search(query, kind?, status?) 例: 「concept:hoge-number を検索」「status=draft の theorem を列挙」 • formath.get(id) / formath.put(entity) / formath.update(id, patch) / formath.delete(id) • formath.link(src_id, dst_id, rel)(依存・参照の明示) • formath.tasks.list(filter) / formath.tasks.upsert(task) / formath.tasks.transition(id, state) • formath.lift_to_lean(entity_ids, target_module) 指定群を Lean ファイルへ射影し、serena で保存、直後に lean-lsp.check 実行 • formath.sync_diagnostics(entity_id) Lean LSP のエラー/ゴールを lean_artifact.lsp_diagnostics に反映
3.2 典型操作 • エンティティ検索: formath.search("Hoge", kind="concept") • properties の列挙/追加/削除: → Formath では Fact を CRUD(追加=新規 Fact、削除=Fact 退役、列挙=search by context/subject)
⸻
エージェント・ワークフロー(TeX→Formath→Lean)
エージェント・ワークフロー(TeX→Formath→Lean)
抽出: TeX(paper.tex)から節/定義/命題/証明を抽出し、Concept/Definition/Fact を作成。source に行範囲・label。
曖昧性解消: 型や既存記号との衝突チェック(Notation/Instance を補完)。
Lean 雛形生成: Definition.lean_stub と Fact.lean_artifact(sorry あり)をまとめて MappingToLean 指定モジュールへ出力。
LSP 検査: lean-lsp で型エラー・未解決インスタンス・不足 import を取得 → lean_artifact.lsp_diagnostics に反映。
証明計画: ProofPlan を生成(simp/library_search/aesop などのタクティク候補を格納)。
自動/半自動証明: ProofStep を試行し、sorry を削減。ゴールスナップショットを記録。
同型整理: 用語の同値や再定式化(iff_characterization)を Fact へ展開し再利用。
ステータス更新: status: checked に昇格、Task をクローズ。
⸻
進捗管理・一時停止/再開
進捗管理・一時停止/再開 • Task エンティティで単位作業を表現(節ごと/lemma ごと)。blockers により待ち順序を明示。 • チェックリスト自動生成: TeX セクションから extract→stub→prove→lint のパイプラインを起票。 • スナップショット: JSONL のコミット(日時・ハッシュ)。IDE(Cursor/Zed)で「前回の成功点」へ簡易ロールバック。 • 部分実行: lift_to_lean([id1,id2]) などで差分だけ再ビルド。
⸻
整合性・検証
整合性・検証 • 型整合: intended_sort と lean_signature の整合を LSP で検査。 • 依存閉包: deps 未解決をビルド前に検知。 • 命名一貫性: name_hints に基づき Lean 名を自動提案(衝突時はサフィックス付与)。 • 出所一貫性: source が未設定のエンティティは status=draft 以上に上げない。 • CI 的検査: imports 最小化、simp セットの安全性、#guard_msgs を活用。
⸻
MVP(最小実装)範囲
MVP(最小実装)範囲 • 必須エンティティ: Concept / Definition / Fact / ProofPlan / Task • ストレージ: formath/ 以下に entities.jsonl(追記型)+ index.sqlite(全文検索用) • MCP: search / get / put / update / tasks.* / lift_to_lean / sync_diagnostics • Lean 側: 1 モジュールへの射影、import Mathlib で完結 • IDE 統合: Cursor/Zed の「スラッシュコマンド or MCP パネル」から呼び出し
⸻
オープン課題
オープン課題 • 証明計画の表現力: 汎用タクティク列 vs. セマンティックな補題適用グラフのどこまでを中間表現に持つか。 • Notation/Instance の自動抽出: TeX と mathlib の橋渡し規約。 • 多言語 TeX/定義文の差: 和文/英文の混在文からの安定抽出。 • 大規模依存: 論文全体/複数章またぎのビルド順最適化。 • 信頼度管理: LLM 提案の信頼度と人手レビューの混在運用。
⸻
運用メモ(実装ヒント)
運用メモ(実装ヒント) • JSONL + 小さなインデックスは衝突少なく扱いやすい。ID は kind:slug 風+内部 UUID が安全。 • Fact 正規化が肝:"hoge number is odd" のような自然文は、Context + Statement に分解して保存。 • Lean 生成は いつでも sorry 可 にしてパイプラインを止めない。エラーは lsp_diagnostics に吸収。 • TeX アンカーは将来の自動再抽出で決定的に重要(\label / 節番号 / 行範囲の三重持ち推奨)。
⸻
Available Tools
14 toolsformalize_texB
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.
| Name | Required | Description | Default |
|---|---|---|---|
| module_name | No | Main | |
| tex_path | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It mentions writing to sibling directories, implying a write operation, but doesn't cover critical aspects like permissions needed, error handling, whether it overwrites existing files, or performance characteristics. This leaves the agent with insufficient information about the tool's behavior.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is extremely concise and front-loaded, with every sentence earning its place. The first sentence defines the pipeline, and the second specifies output locations. There's no wasted verbiage, making it efficient for an agent to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (processing pipeline with file outputs) and no annotations, the description is incomplete. It covers the high-level flow and output destinations but lacks details on error cases, side effects, or dependencies. The presence of an output schema helps, but more behavioral context is needed for a higher score.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the schema provides no parameter details. The description adds some value by implying 'tex_path' is the input TeX file and 'module_name' influences the output Lean module, but it doesn't explain parameter formats, constraints, or defaults. This partial compensation meets the baseline for low coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: it's an end-to-end pipeline that processes TeX files to generate Formath JSONL and Lean stub modules. It specifies the verb ('formalize') and resources (TeX files), though it doesn't explicitly differentiate from sibling tools like 'tex_extract' or 'workflow_formalize_all', which prevents a perfect score.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It mentions output directories but doesn't explain prerequisites, when to choose this over 'tex_extract' or 'workflow_formalize_all', or any constraints. This lack of contextual usage information is a significant gap.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
pingA
Health check tool returning a simple response.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It states the tool returns a 'simple response', implying a read-only, non-destructive operation, but lacks details on response format, latency, error conditions, or side effects. This is adequate for a basic health check but misses richer context.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence that front-loads the key information ('Health check tool') and avoids any wasted words. Every part of the sentence earns its place by clarifying purpose and output.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's simplicity (0 parameters, no annotations, but with an output schema), the description is reasonably complete. It explains what the tool does and what it returns, though it could benefit from more context on typical use cases or response details. The presence of an output schema reduces the need to describe return values in the description.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool has 0 parameters, and the input schema has 100% description coverage (though empty). The description doesn't need to add parameter semantics, so it appropriately focuses on the tool's function. A baseline of 4 is justified as no parameters are present.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose as a 'Health check tool' that returns a 'simple response', which is specific and unambiguous. However, it doesn't explicitly differentiate from sibling tools like 'progress_summary' or 'tasks_list', which might also return status information, so it doesn't fully distinguish from alternatives.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It doesn't mention use cases like verifying server connectivity, testing API availability, or checking system status, nor does it reference sibling tools that might serve similar diagnostic purposes.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
progress_summaryB
Return a compact JSON summary of progress: entity counts and tasks by state.
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It states the tool returns a 'compact JSON summary' but doesn't elaborate on aspects like performance (e.g., speed, data freshness), error handling, or whether it requires specific permissions. For a tool with zero annotation coverage, this is a significant gap in transparency.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is extremely concise and front-loaded, consisting of a single sentence that directly states the tool's purpose and output format. Every word earns its place, with no unnecessary details or redundancy, making it highly efficient for quick understanding.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool has an output schema (which should define the return structure), the description doesn't need to detail return values. However, with no annotations and minimal parameter guidance, it provides only basic purpose and output format. For a tool that likely interacts with project data, this is adequate but leaves gaps in usage context and behavioral traits.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The input schema has one parameter ('project_root') with 0% description coverage, and the tool description doesn't mention any parameters. Since there are zero parameters documented in the description, the baseline score is 4, as the description doesn't need to compensate for schema gaps. However, it misses an opportunity to clarify the optional 'project_root' parameter's role.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Return a compact JSON summary of progress: entity counts and tasks by state.' It specifies the verb ('Return'), resource ('summary of progress'), and key content ('entity counts and tasks by state'). However, it doesn't explicitly differentiate this from sibling tools like 'tasks_list' or 'render_entities_markdown', which might also provide progress-related information.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It doesn't mention sibling tools like 'tasks_list' or 'render_entities_markdown' that might offer similar or overlapping functionality, nor does it specify contexts or prerequisites for usage. This leaves the agent without clear direction on tool selection.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
quickstart_messageB
Return quick instructions for using this server in Cursor.
| Name | Required | Description | Default |
|---|---|---|---|
No parameters | |||
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It states the tool returns instructions, implying a read-only operation, but doesn't disclose behavioral traits like response format, potential errors, or whether it's idempotent. This is a significant gap for a tool with no annotation coverage.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence that front-loads the core purpose with zero waste. Every word earns its place, making it highly concise and well-structured.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's simplicity (0 parameters, output schema exists), the description is minimally adequate. However, with no annotations and an output schema, it could benefit from more context on what the instructions cover or typical use cases, but it's not severely lacking.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The tool has 0 parameters, and schema description coverage is 100%, so no parameter documentation is needed. The description doesn't add parameter details, which is appropriate, earning a baseline score of 4 for this dimension.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Return quick instructions for using this server in Cursor.' It specifies the verb ('Return') and resource ('quick instructions'), though it doesn't explicitly differentiate from siblings like 'ping' or 'progress_summary' which serve different purposes.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives. It doesn't mention prerequisites, context (e.g., for new users), or exclusions, leaving the agent to infer usage based on the purpose alone.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
render_checklist_markdownB
Generate formath/checklist.md from tasks.jsonl (latest per id).
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden. It mentions generating a file but doesn't disclose behavioral traits like whether it overwrites existing files, requires specific permissions, handles errors, or has side effects. For a file-writing tool with zero annotation coverage, this is inadequate.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence with zero waste. It's appropriately sized and front-loaded, directly stating the tool's purpose without unnecessary elaboration.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool has an output schema (which likely describes the generated markdown), the description doesn't need to explain return values. However, for a file-generation tool with no annotations and incomplete parameter semantics, it should provide more context on behavior and usage to be fully complete.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The description adds no information about the single parameter 'project_root'. With 0% schema description coverage and no parameter details in the description, the baseline is 3 since the schema provides the structure but lacks semantic context. The description doesn't compensate for the coverage gap.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Generate') and the specific output resource ('formath/checklist.md'), and identifies the input source ('tasks.jsonl (latest per id)'). It's specific about what the tool does, though it doesn't explicitly differentiate from sibling tools like 'render_entities_markdown' or 'tasks_list'.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool versus alternatives. The description doesn't mention prerequisites, appropriate contexts, or when not to use it. With sibling tools like 'tasks_list' and 'render_entities_markdown' available, this gap is significant.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
render_entities_markdownC
Regenerate formath/entities.md from formath/entities.jsonl for a project.
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries full burden but lacks behavioral details. It states 'Regenerate' which implies a write operation, but doesn't disclose effects (e.g., overwrites existing file, requires specific permissions), response format, or error handling. This is inadequate for a mutation tool with zero annotation coverage.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence that directly states the tool's function without unnecessary words. It's appropriately sized for its purpose, though it could be slightly more informative without losing conciseness.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool has an output schema (which handles return values), the description's main gap is lack of behavioral transparency and parameter details. For a regeneration tool with no annotations, it's minimally adequate but leaves critical aspects like mutation effects and parameter usage unclear, making it incomplete for safe operation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate, but it doesn't mention the 'project_root' parameter at all. The baseline is 3 because the schema covers the parameter structure, but the description adds no value beyond implying a project context, failing to explain parameter meaning or usage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Regenerate') and the specific resource ('formath/entities.md from formath/entities.jsonl'), making the purpose understandable. However, it doesn't explicitly differentiate from sibling tools like 'render_checklist_markdown' or 'tasks_autogen_from_entities', which might involve similar markdown or entity processing, preventing a perfect score.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides minimal guidance, only implying usage when entities.md needs regeneration from entities.jsonl. It offers no explicit when-to-use rules, alternatives (e.g., vs. 'tasks_autogen_from_entities'), or prerequisites, leaving the agent to infer context without clear direction.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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/".
| Name | Required | Description | Default |
|---|---|---|---|
| base_dir | No | ||
| project_name | No | demo |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries full burden. It mentions creating a directory layout with specific components (TeX, rules, placeholders) but doesn't disclose behavioral traits like whether it overwrites existing directories, what permissions are required, error handling, or the structure of created files. The description is functional but lacks operational transparency.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is appropriately sized with a clear purpose statement followed by an Args section. The first sentence efficiently conveys the core functionality, and the parameter explanations are front-loaded and necessary. There's minimal waste, though the structure could be slightly more integrated rather than separate sections.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 2 parameters with 0% schema coverage and no annotations, the description provides basic purpose and parameter semantics. However, as a creation tool with an output schema (implied by context signals), it doesn't explain return values or error conditions. The description is adequate for simple use but lacks depth for complex scenarios like handling existing directories or detailed output.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate. The Args section adds meaningful semantics: it explains that project_name creates a directory and that base_dir is optional with a default location. This clarifies parameter roles beyond the schema's basic titles, though it doesn't detail format constraints or examples.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the specific action ('Create a minimal formalization project layout') and specifies the resources involved ('with TeX, rules, and placeholders'). It distinguishes from sibling tools like 'formalize_tex' or 'workflow_formalize_all' by focusing on initial project scaffolding rather than content processing or comprehensive workflows.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage context through 'minimal formalization project layout' and the Args section mentions default behavior for base_dir. However, it doesn't explicitly state when to use this tool versus alternatives like 'quickstart_message' or 'workflow_formalize_all', nor does it provide exclusions or prerequisites for usage.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| kind | No | fact | |
| project_root | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. It mentions that the tool 'Returns number of tasks created,' which is useful, but fails to describe other critical behaviors such as permissions needed, whether it modifies existing data, error handling, or rate limits. For a tool that creates tasks, this omission is significant and reduces transparency.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is highly concise and front-loaded, consisting of two sentences that directly state the tool's function and return value. Every sentence earns its place by providing essential information without redundancy, making it efficient and easy to parse for an agent.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's complexity (task creation with 2 parameters), no annotations, and an output schema (which likely covers return values), the description is minimally adequate. It explains the core purpose and return, but lacks details on behavioral traits, parameter nuances, and usage context, leaving gaps that could hinder an agent's effective use.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The description adds some semantic context: it explains that 'kind' defaults to 'fact' (lemmas) and implies it filters entities without tasks. However, with 0% schema description coverage and 2 parameters, it does not fully compensate by detailing the purpose or format of 'project_root' or other aspects of 'kind.' The baseline is 3 due to the schema's lack of descriptions, but the description provides only partial compensation.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose: 'Create open tasks for entities of given kind that do not already have tasks.' It specifies the verb ('create'), resource ('open tasks'), and target ('entities of given kind'), making the intent understandable. However, it does not explicitly differentiate this tool from its siblings like 'tasks_list' or 'tasks_upsert', which slightly limits its clarity in a broader context.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage by mentioning 'entities of given kind that do not already have tasks,' suggesting it should be used to generate tasks for untasked entities. However, it lacks explicit guidance on when to use this tool versus alternatives like 'tasks_upsert' or 'tasks_list,' and does not specify prerequisites or exclusions, leaving some ambiguity for the agent.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
tasks_listC
List tasks (optionally filter by state). Returns JSON list (latest per id).
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No | ||
| state | No |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries full burden for behavioral disclosure. It mentions the return format ('JSON list') and a behavioral detail ('latest per id'), which adds value. However, it doesn't address important aspects like whether this is a read-only operation, pagination behavior, rate limits, authentication requirements, or what happens with the 'project_root' parameter. The description provides some behavioral context but leaves significant gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is efficiently structured in a single sentence that front-loads the core purpose. Every element ('List tasks', 'optionally filter by state', 'Returns JSON list (latest per id)') serves a purpose. It could be slightly more structured but achieves conciseness without wasted words.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 2 parameters with 0% schema coverage, no annotations, but an output schema exists, the description is minimally adequate. The output schema means return values don't need explanation, but the description should better explain parameter usage and behavioral context. It covers basic purpose and return format but leaves parameter semantics and usage guidelines underdeveloped.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate. It mentions filtering by 'state' but doesn't explain what states are available or how filtering works. It completely ignores the 'project_root' parameter. The description adds minimal semantic value beyond what's inferable from parameter names, failing to compensate for the schema's lack of descriptions.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb ('List') and resource ('tasks'), and mentions optional filtering by state. It distinguishes from some siblings like 'tasks_upsert' (create/update) and 'tasks_transition' (change state), but doesn't explicitly differentiate from 'tasks_pick_next' or 'tasks_autogen_from_entities'. The purpose is specific but sibling differentiation is incomplete.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives like 'tasks_pick_next' (which likely selects specific tasks) or 'progress_summary' (which might summarize task states). It mentions optional filtering by state but doesn't explain when filtering is appropriate or what alternatives exist for different query needs.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
tasks_pick_nextB
Mark next open tasks as in_progress (up to limit). Returns transitioned ids.
| Name | Required | Description | Default |
|---|---|---|---|
| limit | No | ||
| project_root | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden but only states the basic action and return. It doesn't disclose permissions needed, whether this is idempotent, how 'next open tasks' are determined (e.g., priority, creation time), error handling, or side effects beyond the state change.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
Extremely concise single sentence with zero waste, front-loading the core action. Every word earns its place by specifying the operation, scope, and return value efficiently.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 2 parameters with 0% schema coverage, no annotations, but an output schema (which handles return values), the description is minimally adequate. It covers the basic purpose and output but lacks parameter semantics and behavioral context needed for safe invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate but adds no parameter details. It mentions 'limit' generally but doesn't explain the 'project_root' parameter at all or provide format/constraints for either parameter beyond what's in the schema (which has minimal descriptions).
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Mark next open tasks as in_progress') and resource ('tasks'), with specific scope ('up to limit') and outcome ('Returns transitioned ids'). It distinguishes from siblings like tasks_list (list) and tasks_transition (general transition), but doesn't explicitly name alternatives.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage when needing to advance tasks to in_progress state with a limit, but doesn't specify when to use this vs. tasks_transition (which might handle arbitrary transitions) or tasks_autogen_from_entities. No explicit when-not or alternative guidance is provided.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
tasks_transitionC
Append a state transition record for a task id.
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No | ||
| state | Yes | ||
| task_id | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries full burden but only states the action ('append') without disclosing behavioral traits like whether this is a mutation (likely yes, given 'append'), permission requirements, side effects (e.g., if it modifies task status or just logs), rate limits, or response format. It lacks critical context for safe invocation.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, efficient sentence with zero waste, front-loading the core action. It's appropriately sized for the tool's apparent complexity, though brevity contributes to gaps in other dimensions.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 3 parameters, no annotations, and an output schema (which reduces need to explain returns), the description is minimally complete but lacks detail on mutation behavior, parameter meanings, and usage context. It's adequate for basic understanding but has clear gaps for effective tool selection.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate but adds no parameter semantics. It mentions 'task id' and 'state' implicitly but doesn't explain their roles, formats, or constraints (e.g., valid state values, what project_root does). With 3 parameters and low coverage, this is inadequate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description 'Append a state transition record for a task id' specifies the action (append) and resource (state transition record for a task), but it's vague about what 'append' means operationally (e.g., adds to a log vs. updates a field) and doesn't distinguish it from siblings like tasks_upsert or tasks_list. It avoids tautology by not restating the name/title.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is provided on when to use this tool versus alternatives such as tasks_upsert (which might update task states) or tasks_list (for viewing states). The description implies usage for recording state changes but doesn't specify prerequisites, exclusions, or contextual triggers.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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
| Name | Required | Description | Default |
|---|---|---|---|
| project_root | No | ||
| task | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It usefully describes the return value ('Returns the task id') and provides important context about the flexible task shape and valid states. However, it doesn't address critical behavioral aspects like whether this is an idempotent operation, what happens with partial updates, authentication requirements, error conditions, or rate limits. The disclosure is helpful but incomplete for a mutation tool.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is efficiently structured with zero wasted words. The first sentence states the core purpose and return value, followed by essential details about the task shape and states. Every sentence earns its place, and information is front-loaded appropriately for quick comprehension.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given this is a mutation tool with no annotations, 2 parameters (0% schema coverage), nested objects, and an output schema, the description provides a reasonable baseline. The output schema likely documents the return structure, so the description's focus on the task id is sufficient. However, for a flexible upsert operation with undocumented parameters, more guidance on parameter usage and behavioral expectations would improve completeness.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
With 0% schema description coverage for both parameters, the description fails to compensate for this gap. While it mentions the 'task' parameter shape and states, it doesn't explain the 'project_root' parameter at all or provide details about the 'task' object structure beyond a basic outline. The description adds some value about task fields but leaves significant parameter semantics undocumented.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the verb ('Create or update') and resource ('a task'), making the purpose immediately understandable. It distinguishes this tool from siblings like 'tasks_list' (read-only) and 'tasks_transition' (state changes only), though it doesn't explicitly name those alternatives. The mention of returning 'the task id' adds useful outcome information.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage context through 'Create or update a task' and mentions the flexible task shape, suggesting this is the primary tool for task creation/modification. However, it doesn't explicitly state when to use this versus alternatives like 'tasks_autogen_from_entities' or 'tasks_transition', nor does it mention prerequisites or exclusions. The guidance is functional but lacks comparative clarity.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
tex_extractB
Extract definitions and lemmas from a TeX file. Returns a compact JSON summary.
| Name | Required | Description | Default |
|---|---|---|---|
| tex_path | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full burden of behavioral disclosure. It mentions the return format ('compact JSON summary'), which adds some value, but fails to address critical aspects like error handling, performance, or whether the operation is read-only or has side effects. This leaves significant gaps in understanding the tool's behavior.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is extremely concise and front-loaded, consisting of just two sentences that directly state the action and output. Every word earns its place, with no unnecessary information, making it efficient and easy to parse.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given the tool's moderate complexity (extracting from TeX files), no annotations, and an output schema that likely covers return values, the description is minimally adequate. It specifies the action and output format, but lacks details on behavioral traits and parameter semantics, leaving room for improvement in completeness.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
The description does not add any semantic details about the single parameter 'tex_path' beyond what the input schema provides (which has 0% coverage, as the schema lacks descriptions). Since there is only one parameter, the baseline is 4, but the description fails to compensate for the schema's lack of detail, such as explaining what 'tex_path' represents or any format requirements, resulting in a reduced score.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the tool's purpose with a specific verb ('extract') and resource ('definitions and lemmas from a TeX file'), making it easy to understand what it does. However, it doesn't explicitly differentiate from sibling tools like 'formalize_tex', which might have overlapping functionality, preventing a perfect score.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides no guidance on when to use this tool versus alternatives, such as 'formalize_tex' or other siblings. It lacks context about prerequisites, constraints, or specific scenarios where extraction is preferred over other operations, leaving the agent to infer usage.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
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.
| Name | Required | Description | Default |
|---|---|---|---|
| naming | No | by_file | |
| project_root | Yes |
Output Schema
| Name | Required | Description |
|---|---|---|
| result | Yes |
TDQS
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries full burden for behavioral disclosure. It mentions the return format ('JSON array of results per file') and naming behavior, which adds some context. However, it doesn't describe what 'formalize' entails operationally (e.g., what transformations occur), potential side effects, error handling, or performance characteristics. For a batch processing tool with zero annotation coverage, this leaves significant behavioral gaps.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is extremely concise with only three sentences, each delivering essential information: scope, parameter behavior, and return format. It's front-loaded with the core action and wastes no words. The structure efficiently communicates key details without redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
Given 2 parameters, 0% schema coverage, no annotations, but with an output schema (which handles return values), the description provides adequate context. It covers the tool's scope, parameter semantics for naming, and output structure. However, it lacks details on what 'formalize' means operationally and any prerequisites, which would be helpful given the complexity of batch file processing.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 0%, so the description must compensate. It explains the 'naming' parameter's behavior ('by_file' → module name from file stem, otherwise use "Main") and implies 'project_root' specifies the directory path. This adds meaningful semantics beyond the bare schema, though it doesn't detail parameter constraints or formats. With 2 parameters and good clarification of the optional one, it earns above baseline.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description clearly states the action ('Formalize all *.tex') and target resource ('under <project_root>/tex'), making the purpose understandable. It distinguishes from sibling 'formalize_tex' by indicating batch processing of all files rather than a single file, though it doesn't explicitly name the alternative. The description avoids tautology and provides specific scope information.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description implies usage context through the project_root parameter and the 'all *.tex' scope, suggesting this is for batch processing of LaTeX files in a project. However, it doesn't explicitly state when to use this versus 'formalize_tex' or other siblings, nor does it provide prerequisites or exclusions. The guidance is functional but lacks explicit comparative direction.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Tool Schema Changelog
Recent tool additions, removals, and schema changes observed during successful MCP inspections. Dates show when Glama detected each change.
14 tool updates
v1.0.0- First observed
formalize_tex - First observed
ping - First observed
progress_summary - First observed
quickstart_message - First observed
render_checklist_markdown - First observed
render_entities_markdown - First observed
scaffold_project - First observed
tasks_autogen_from_entities - First observed
tasks_list - First observed
tasks_pick_next - First observed
tasks_transition - First observed
tasks_upsert - First observed
tex_extract - First observed
workflow_formalize_all
TDQS
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.
Resources
Unclaimed servers have limited discoverability.
Looking for Admin?
If you are the server author, to access and configure the admin panel.
Related MCP Connectors
Search arXiv/Semantic Scholar/OpenAlex + medical evidence (PubMed/Europe PMC) + LaTeX/PDF tools.
High-fidelity PDF to structured Markdown conversion and document field extraction.
Persistent AI LaTeX workspace: edit and compile multi-file projects, export publication-ready PDFs.
Extract structured data points from research papers and other documents with an LLM.
Related MCP Servers
- AlicenseBqualityFmaintenanceIntegrates Jina.ai's Reader API with LLMs for efficient and structured web content extraction, optimized for documentation and web content analysis.13829MIT
- AlicenseBqualityFmaintenanceEnables retrieval and processing of web page content for LLMs by converting HTML to markdown, with support for content truncation and pagination.13MIT
- -licenseBqualityNot gradedmaintenanceAutomates the creation of standardized documentation by extracting information from source files and applying templates, with integration capabilities for GitHub, Google Drive, and Perplexity AI.33-
- AlicenseAqualityBmaintenanceFast, token-efficient web content extraction tool that converts websites to clean Markdown for AI agents, featuring smart caching, content extraction with Mozilla Readability, and polite crawling capabilities.1534161MIT
Appeared in Searches
Latest Blog Posts
- Who's Calling? MCP Hosts Are an Identity Blind Spot (And the Spec Knows It)By Om-Shree-0709 on .mcpAgent IdentityOAuth 2.1
- Your AI Chatbot Just Exposed Your CEO's Salary to an InternBy Om-Shree-0709 on .Agent IdentityMCP SecurityOAuth Delegation
- Why MCP Servers Need Execution Sandboxing (And Why Your Current Stack Isn't Enough)By Om-Shree-0709 on .Agentic AiPrompt InjectionWebAssembly
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