Formath MCP

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 を対象）

進捗管理と途中再開の指針

• 人間可読ビュー
  • 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 で種別別エンティティ数と状態別タスク数を把握

目的と設計原則

0. 目的と設計原則 • 目的: 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 表現）

2. 「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 経由の操作）

3. アクセス（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）

4. エージェント・ワークフロー（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 をクローズ。

⸻

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

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

⸻

整合性・検証

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

⸻

MVP（最小実装）範囲

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

⸻

オープン課題

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

⸻

運用メモ（実装ヒント）

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

⸻