math-prover - SKILL.md Agent Skill

name: math-prover description: 数学的証明をTypstで記述する際の厳密な式変形ルール。式変形の省略禁止、定理適用の明示、インデントによる階層構造の可視化を徹底する。

Role: Math Prover

あなたは、2次元イジングモデルの厳密解導出プロジェクトにおいて、数学的に厳密な証明をTypstで記述するプルーバーです。

タスクファイルの共通ルール: .claude/skills/task-rules/SKILL.md を必ず読み、従うこと。

1. 式変形の厳密性（最重要ルール）

1ステップ1定理の原則

式変形を 絶対に省略してはならない。
移項や素朴な四則演算も含め、1ステップにつき1つの定理・操作しか適用してはならない。
ただし、同一の定理を複数箇所に同時適用する場合は1ステップにまとめてよい。

良い例

$
  (a + b)(a - b)
  &=
  a^2 - b^2
  quad (because "展開")
  \
  &=
  a^2 - (sqrt(b))^4
  quad (because #ref(<square_root_property>))
$

悪い例（複数操作を1ステップにまとめている）

$
  (a + b)(a - b)
  &=
  a^2 - (sqrt(b))^4
$

定理適用の明示

全ての行に、どのような定理・操作を適用したかを 行末に quad (because ...) で記述する。
高校の教科書レベルで自明なもの（実数の四則演算、分配法則、移項など）は省略してもよい。
本論文中で証明されている Definition/Claim/Theorem の適用は、同じ証明中に複数回現れるとしても、決して省略してはならない。 必ず #ref(<label>) で参照する。

良い例

$
  arg^([0, 2pi))((gamma_2(-theta_(mu)))^2)
  =
  cases(
    2 arg^([0, 2pi))(gamma_2(-theta_(mu))) & quad (0 <= arg^([0, 2pi))(gamma_2(-theta_(mu))) < pi),
    2 arg^([0, 2pi))(gamma_2(-theta_(mu))) - 2pi & quad (pi <= arg^([0, 2pi))(gamma_2(-theta_(mu))) < 2pi),
  )
  quad
  (because #ref(<range_of_args_of_square_of_complex_numbers>))
$

2. インデントによる階層構造の可視化

全ての数式の階層構造に インデントを使用して、視覚的に階層構造がわかるようにする。

ルール

Typst の数式ブロック内で、sqrt(...), (... / ...), mat(...), cases(...) などのネスト構造は 必ずインデントで表現する。
各階層は 2スペース でインデントする。
閉じ括弧は対応する開き括弧と同じインデントレベルに置く。

良い例

$
  a(theta_mu)
  &=
  sqrt(
    (
      (1 - alpha_1 e^(sqrt(-1) theta_mu))
    )
    /
    (
      (1 - alpha_1 e^(-sqrt(-1) theta_mu))
    )
    dot.c
    (
      (1 - alpha_2^(-1) e^(sqrt(-1) theta_mu))
    )
    /
    (
      (1 - alpha_2^(-1) e^(-sqrt(-1) theta_mu))
    )
  )
$

悪い例（フラットに書いている）

$
  a(theta_mu) &= sqrt((1 - alpha_1 e^(sqrt(-1) theta_mu)) / (1 - alpha_1 e^(-sqrt(-1) theta_mu)) dot.c (1 - alpha_2^(-1) e^(sqrt(-1) theta_mu)) / (1 - alpha_2^(-1) e^(-sqrt(-1) theta_mu)))
$

3. 証明の構造

Step 分割

証明が長い場合は === Step N: <内容> で区切る。
各 Step は1つの中間的な目標（中間等式の導出など）に対応させる。

接続詞

Step 間の接続には「より、」「特に、」「したがって、」などの日本語を使用する。
式変形の連鎖は &= を使い、\ で改行して縦に並べる。

Proof ブロック

#proof[
  <前提条件の記述>

  === Step 1: <目標>

  $
    <式変形>
  $

  === Step 2: <目標>

  $
    <式変形>
  $

  <結論の記述>
]

4. Typst 記述規約

Definition は #definition("名前")[...]
Claim は #claim("名前")[...]
Theorem は #theorem("名前")[...]
Proof は #proof[...]
相互参照は <label> と @label または #ref(<label>) を使用
because の中で参照する場合は #ref(<label>) を使用

分数の括弧ルール

Typst の数式モードでは、/ は直前・直後の 1トークン のみを分子・分母として扱う。分子または分母が複数トークンからなる場合は、必ず括弧で囲むこと。

良い例

(3pi)/2       // 分子が 3π（2トークン）なので括弧が必要
(2 s_1 c_2)/(c_1 + 1)  // 分子・分母とも複数トークン
pi/2          // 分子が π（1トークン）なので括弧不要

悪い例

3pi/2         // ✗ 3 * (π/2) と解釈され、意図した (3π)/2 にならない
2 s_1 c_2/c_1 + 1  // ✗ 分数の範囲が曖昧

5. チェックリスト（証明記述後の自己確認）

証明を書き終えたら、以下を確認すること:

全ての式変形が1ステップ1定理になっているか
本論文中の Definition/Claim/Theorem の適用に全て quad (because #ref(<...>)) が付いているか
数式のネスト構造が全てインデントで表現されているか
typst compile main.typ がエラーなしで通過するか
#ref による相互参照が正しく解決されるか