Skip to main content
Glama

Formath MCP

by yutayamamoto

Overview of Formath

Minimal MCP quickstart

  1. Install deps: uv sync
  2. Run server: uv run main.py
  3. In 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 を登録済み、サーバーが起動済み
  • 手順:
    1. ヘルスチェック: formath-mcp.ping() → "pong"
    2. 抽出(件数と概要を把握):
      • formath-mcp.tex_extract("/Users/yutayamamoto/repo/formath-mcp/projects/demo1/tex/paper2.tex")
      • 返り値に definitions/lemmas の件数とサンプルを含む JSON が返る
    3. 形式化(最小雛形生成):
      • 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 安全な識別子に自動変換)
    4. IDE で Paper2.lean を開いて雛形を確認(必要に応じて LSP/ビルドで診断)
    5. 参考: 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 で種別別エンティティ数と状態別タスク数を把握

目的と設計原則

  1. 目的と設計原則 • 目的: TeX 論文から抽出した数学的内容を、LLM/エージェントが 一貫性ある中間表現(Formath) に整理し、Lean コードへ段階的に落とし込む。 • 原則
    1. 人手最小・再開容易(途中停止/再開・差分実行・履歴管理)
    2. Lean 忠実(型・文脈・インスタンス・記法を明示)
    3. 出所管理(TeX の箇所へのアンカーと生成/検証の由来)
    4. 段階分離(NL→Formath→Lean を明確に分離)
    5. グラフ構造(概念間依存関係・仮定コンテキストを明示)

コア・データモデル(エンティティ)

  1. コア・データモデル(エンティティ)

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 表現)

  1. 「hoge number」例(最小 MVP 表現)

{"id":"concept","kind":"concept","title":"hoge number", "symbols":[{"name":"Hoge","latex":"\mathrm{Hoge}","role":"pred","arity":1}], "intended_sort":"Nat","canonical_definition":"def","examples":[ {"term_text":"11"},{"term_text":"12"},{"term_text":"13"}], "source":{"file":"paper.tex","span":"L120-160","label":"def"}}

{"id":"def","kind":"definition","title":"def of hoge number", "concept_id":"concept", "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","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 経由の操作)

  1. アクセス(MCP 経由の操作)

serena(ファイル IO)、lean-lsp(型チェック/ゴール取得)、独自 MCP formath を想定。

3.1 formath MCP(例) • formath.search(query, kind?, status?) 例: 「concept を検索」「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)

  1. エージェント・ワークフロー(TeX→Formath→Lean)
    1. 抽出: TeX(paper.tex)から節/定義/命題/証明を抽出し、Concept/Definition/Fact を作成。source に行範囲・label。
    2. 曖昧性解消: 型や既存記号との衝突チェック(Notation/Instance を補完)。
    3. Lean 雛形生成: Definition.lean_stub と Fact.lean_artifact(sorry あり)をまとめて MappingToLean 指定モジュールへ出力。
    4. LSP 検査: lean-lsp で型エラー・未解決インスタンス・不足 import を取得 → lean_artifact.lsp_diagnostics に反映。
    5. 証明計画: ProofPlan を生成(simp/library_search/aesop などのタクティク候補を格納)。
    6. 自動/半自動証明: ProofStep を試行し、sorry を削減。ゴールスナップショットを記録。
    7. 同型整理: 用語の同値や再定式化(iff_characterization)を Fact へ展開し再利用。
    8. ステータス更新: status: checked に昇格、Task をクローズ。

進捗管理・一時停止/再開

  1. 進捗管理・一時停止/再開 • Task エンティティで単位作業を表現(節ごと/lemma ごと)。blockers により待ち順序を明示。 • チェックリスト自動生成: TeX セクションから extract→stub→prove→lint のパイプラインを起票。 • スナップショット: JSONL のコミット(日時・ハッシュ)。IDE(Cursor/Zed)で「前回の成功点」へ簡易ロールバック。 • 部分実行: lift_to_lean([id1,id2]) などで差分だけ再ビルド。

整合性・検証

  1. 整合性・検証 • 型整合: intended_sort と lean_signature の整合を LSP で検査。 • 依存閉包: deps 未解決をビルド前に検知。 • 命名一貫性: name_hints に基づき Lean 名を自動提案(衝突時はサフィックス付与)。 • 出所一貫性: source が未設定のエンティティは status=draft 以上に上げない。 • CI 的検査: imports 最小化、simp セットの安全性、#guard_msgs を活用。

MVP(最小実装)範囲

  1. 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 パネル」から呼び出し

オープン課題

  1. オープン課題 • 証明計画の表現力: 汎用タクティク列 vs. セマンティックな補題適用グラフのどこまでを中間表現に持つか。 • Notation/Instance の自動抽出: TeX と mathlib の橋渡し規約。 • 多言語 TeX/定義文の差: 和文/英文の混在文からの安定抽出。 • 大規模依存: 論文全体/複数章またぎのビルド順最適化。 • 信頼度管理: LLM 提案の信頼度と人手レビューの混在運用。

運用メモ(実装ヒント)

  1. 運用メモ(実装ヒント) • JSONL + 小さなインデックスは衝突少なく扱いやすい。ID は kind 風+内部 UUID が安全。 • Fact 正規化が肝:"hoge number is odd" のような自然文は、Context + Statement に分解して保存。 • Lean 生成は いつでも sorry 可 にしてパイプラインを止めない。エラーは lsp_diagnostics に吸収。 • TeX アンカーは将来の自動再抽出で決定的に重要(\label / 節番号 / 行範囲の三重持ち推奨)。

Related MCP Servers

  • A
    security
    A
    license
    A
    quality
    Integrates Jina.ai's Reader API with LLMs for efficient and structured web content extraction, optimized for documentation and web content analysis.
    Last updated -
    47
    31
    MIT License
    • Linux
  • A
    security
    A
    license
    A
    quality
    Enables retrieval and processing of web page content for LLMs by converting HTML to markdown, with support for content truncation and pagination.
    Last updated -
    1
    2
    MIT License
  • A
    security
    A
    license
    A
    quality
    Automates the creation of standardized documentation by extracting information from source files and applying templates, with integration capabilities for GitHub, Google Drive, and Perplexity AI.
    Last updated -
    3
    3
    MIT License
    • Apple
  • A
    security
    A
    license
    A
    quality
    Fast, 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.
    Last updated -
    1
    514
    77
    MIT License

View all related MCP servers

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