lean-formalize

Lean の形式化

各レビュアースロットの前に、選択可能なレビュアーに従ってください。 呼び出し設定 → .aris/reviewer.json → Claude Code のデフォルト（Codex MCP）の順に解決し、 正規のヘルパーリゾルバーを通じて reviewer_route.py を使用してください。その際、この スロットのティア、新しいコンテキスト、ソース／画像入力、決定論的なゲートを維持してください。 以下の Codex の例／固定指定は backend=codex にのみ適用されます。それ以外のルートでは、 それぞれ独自の初回呼び出し／応答の契約が適用されます。ルートと実際に返された ID を保存してください。 選択したレビュアーが利用できない場合は REVIEW_UNAVAILABLE とします。実際の ファミリー／完了状況／スコープに基づいて受け入れ可否を分類してください。レビュアーを伴う 子タスクには、呼び出し時のレビュアー／モデル／推論強度のオーバーライドを引き継いでください。 生成ワーカーに変更はありません。

ユーザーの数学的な命題の意味を保ったまま、検証済みの Lean の定理に変換します。コンパイルできる条件付き補題も進捗ですが、完了の判断では、元の命題と実際に用いた信頼基盤を対象とします。

Lean を使う場面

ユーザーが Lean を依頼した場合、既存の Lean 証明を続ける場合、または形式検証によって中心的な主張に関する具体的な不確実性を解消できる場合に、このスキルを使用してください。たとえば、長い依存関係の連鎖、慎重な簡約、有限分類の網羅性などが該当します。解消に役立つ義務を明示し、許可されたタスクの範囲内で進めてください。難しいというだけでは形式化の理由になりません。通常の導出や短い証明は formula-derivation または proof-writer で進められます。すべての数学的結果に Lean を必須としないでください。ユーザーが選んだ証明方法と依頼された作業の規模を尊重してください。

基本ワークフロー

Original statement and Lean definitions
  → A: cross-family adversarial statement alignment
  → Proof obligations, representations, and lemma interfaces
  → Lean implementation ↔ B: adversarial review of key arguments and connections
  → Actual inputs connected; original theorem assembled
  → Executed type, definition, and transitive-axiom audit
  → C: cross-family adversarial review of the final exported result
  → Reproducible delivery and research-state update

新たに行う大規模な証明プロジェクトでは、A/B/C がワークフローの一部です。継続作業では、変更のない主張に対して完了済みの検証を再利用し、影響を受ける箇所を再確認してください。小規模で定型的な形式化では、実際の主張に応じた検証を行ってください。ただし、ファミリー横断レビューをユーザーが明示的に依頼している場合は、小規模な形式化でも実施してください。

現在のホストで利用可能な、許可されたレビュアーファミリーを使用してください。ユーザーが Grok と Gemini の両方を指定した場合は、両方からレビューを取得して記録してください。同じファミリーのエージェントや別のプロバイダーで、どちらかの指定を暗黙に満たしたことにしてはいけません。利用できない場合、そのチェックポイントは保留のままにし、独立した証明作業を続けてください。検証済みの定理と、依頼されたレビュー手順をすべて完了することは、それぞれ別の成果物です。

スコープと着手

依頼された範囲に従ってください。実装、継続、監査、パッケージ化のいずれかを行います。監査では、黙って修正したり定理を弱めたりせず、調査して報告してください。実装では、Lean の証明だけでなく数学的な議論も組み立ててください。関連文献やライブラリの結果を調べ、別の方針を検討し、不足する補題を証明してください。残りのインターフェースとトップレベルの組み立てまで続け、目標の宣言や最初のコンパイル成功だけで止めないでください。

権威ある命題、既存の Lean エントリーポイント、ツールチェーン、ロックファイル、最新の進捗記録を確認してください。プロジェクトとその文書名を再利用してください。既存環境が適切な場合は、ツールを再インストールしたり、依存関係を変更したり、新しい証明フレームワークを立ち上げたりしないでください。固定されたライブラリに照らして API を確認してください。

既存の証明方針が機能する場合は、それを使用してください。数学的な議論自体が欠けている場合は、その義務を切り分けて、proof-writer または通常の証明作業を使用してください。委任された proof-writer タスクでは、その議論を構築し、証明または残っている課題をこの実行に返してください。lean-formalize を再度呼び出してはいけません。構文の自動化では、証明されていない前提を解消できません。任意の未解決問題を形式化または解決できると約束しないでください。

適切な作業を開始または再開する

現在の入力	最初に役立つアクション
数学的な命題のみ	定義と量化子を確定し、証明の方針と最初の難しい証明義務を組み立てる
文章による証明	自明でない依存関係を特定し、Lean での表現を選び、コードを書く前に不足している論証を明らかにする
部分的な Lean プロジェクト	対象と実際の呼び出し元を調べ、直近で役立つビルド／エラー記録を読み、未解決の接続のうち最も上位の箇所から続ける
監査依頼	定義とエクスポートされた型を読み、該当するチェックを実行して報告する。対象を黙って修正しない
引き継ぐための完成済みの証明	現在のエントリーポイントと根拠を確認し、数学的な探索をやり直さずに、移植可能なソースとコマンドを用意する

意図するメインモジュール、エクスポートする宣言、現在の次の証明義務を 早い段階で明示してください。完全な数学的方針がまだ分からない場合は、 どの命題に取り組んでいるのかを述べてください。実装が始まったというだけで、 証明可能だと判断してはいけません。 ツール／API の問題と、数学的な論証の不足とでは、次の対応が異なります。

1. 実装の前に意味を確定する

短い数学的仕様を記録するか、既存の仕様を参照してください。

• 対象、定義域、量化子、元の仮定、結論。
• 便宜上の表現と元の対象との同値性。
• 計算、外部証明書、論理的基盤に関するユーザーの制約。
• 結果を表現し証明するために想定する Lean の宣言。

元の仮定と、帰着によって導入される性質を区別してください。有限性、 非空性、決定可能性、正規化、添字規約が命題をどのように変えるか、 または橋渡しが必要になる箇所を特定してください。無関係な端のケースを 作り出すのではなく、実際の定理における自明化や量化子の不備の可能性を 確認してください。

ユーザーが目標を変更するまでは、ユーザーの元の命題を比較の基準として 維持してください。実装に合わせて書き換えた作業用仕様をもって、 その基準を変更してはいけません。許可されたスコープの変更は明示的に記録し、 セッション中にすでに許可された変更について再度確認を求めないでください。 修正によって得られたのが、より強い仮定またはより弱い結論にすぎない場合は、 証明された変種と、依然として未解決の元の証明義務を特定してください。 より強い結果から元の主張を導く含意が提示されれば、元の主張を確立できる 場合があります。

実際の定義本体と提案された目標について、チェックポイント A を実行して ください。元の数学と比較する前に、独立した逆翻訳を求めてください。 入力パケットとプロンプトは references/adversarial-review.md にあります。意図された文章だけを読んだレビュー担当者は、形式化の内容を 確認したことにはなりません。

2. 接続を設計してから、有用な要素を構築する

任意の元の入力から結論までの道筋を整理します。重要なインターフェースごとに、次の内容を記録します。

宣言／義務	前提としていること	実際の入力の出所	根拠／残された課題
条件付きの結果	追加の仮定	元の入力から得られる、名前付きの構成または定理	実際の状態

未解決の接続のうち、最も重要なものを優先します。特に、次の3点を区別してください。

1. 数式または証明書が目的の数を計算する。
2. 実際の数学的対象が、その数式または証明書を実現する。
3. 計算された事実が、元の結論を導く。

3つすべてに個別の証明が必要な場合があります。目的の性質をフィールドとして格納する構造体、提示された確率境界、または結論と同値な仮定を用いても、その入力を構成する義務はなくなりません。

条件付き補題を開発用のインターフェースとして使い、その旨を明記します。不完全な試行は、認証対象の依存関係から外しておきます。一時的な sorry は未完了の作業として見える状態にし、最終的な対象の監査まで残してはいけません。エラー箇所を特定できる程度には中間コンパイルを行いますが、ファイル数や証明済みの算術命題を、完了したことの根拠とみなしてはいけません。

並行作業は、安定した補題シグネチャとモジュールの担当範囲に沿って分割します。各担当者に、仮定、結論、依存関係、および具体的なコンパイル対象を示します。台帳を閉じる前に、成果を実際の呼び出し元と照らし合わせて統合します。並行作業の担当者が、証明に都合がよいように共有オブジェクトをひそかに再定義することがないようにします。

実装ループ

義務を実装または修正する際は、references/lean-working-loop.md を読んでください。この資料では、検索 → 実際の呼び出し元での実験 → 診断 → 修正のサイクルを、表現の選択やパフォーマンス上の問題も含めて解説し、コンパイル済みライブラリをアプリケーションで使う例を示しています。

1. 主定理が証明できる内容を変える、未解決の接続または数学的補題を選びます。その正確な Lean インターフェースと、呼び出し元が満たすべき義務を明示します。
2. 固定されたライブラリとプロジェクトで必要な結果を探します。見慣れない宣言は #check でローカルに確認し、実際のボトルネックを簡単にできる場合は、既存の同等な表現を使います。
3. 補題と実際の使用箇所を実装します。影響を受けるモジュールをコンパイルし、統合後は、その状態がこの補題に依存する下流のターゲットをコンパイルします。
4. 最初に関連するエラーを診断します。エラボレーション／API の不一致なら、ローカルな実装を修正します。利用できない仮定があるなら、その導出、別の論証、または明示的に残された数学的義務が必要です。
5. 有限な場合分けの計算が高コストになったら、一般的な計数補題、漸化式、またはより小さな検証済み証明書を検討します。タクティクが完了するようにするだけの目的で、信頼基盤を黙って拡大してはいけません。
6. 新たに証明を支える議論またはインターフェースに到達したら、チェックポイント B を実行します。有効な修正を実装してコンパイルし、変更された義務についてフォローアップを依頼します。
7. 宣言、実際の呼び出し元、検証の証拠、残っている前提を既存の台帳に記録し、次の接続に進みます。

たとえば、型 Certificate x → Desired x の定理が役立つのは、プロジェクトが必要とするすべての元の入力について Certificate x を構成できる場合に限られます。その構成を完了し、呼び出し元と接続することは、条件付き定理を証明することとは別個の成果です。カーネルによる検査では、パラメーターの型名がもっともらしいというだけで、そのパラメーターが解消されることはありません。

タイマー、変更のないビルドの繰り返し、またはモデル呼び出しの繰り返しを、進捗の代わりに使わないでください。具体的な失敗の後は、正当化できる別の表現または証明経路を試し、依頼された作業をまだ完了できない場合は、正確な阻害要因を残してください。実装の失敗、中間的な主張の失敗、手法全体に対する障害を区別してください。うまくいかなかった経路は、その理由とともに打ち切ってください。その経路を退けても、元の定理が反証されたことにはなりません。提案するアプローチが異なる理由で失敗しうる場合に、並行して探索するのが最も有効です。

3. 証明済みの解釈を伴う計算を使う

有限個の例、証明済みの領域全体に対する網羅的計算、検証済み証明書、記号的／一般的な証明を区別してください。範囲を限定した探索は、その探索対象についての証拠です。網羅性、エンコーディングとの対応、検証手順が確立され、ユーザーの制約が許す場合、有限領域の網羅的な検証は証明になりえます。エンドツーエンドの Lean の結果では、網羅性と解釈自体が、宣言された基盤の下で証明済みの依存関係チェーンに含まれていなければなりません。有限リストが網羅的だとコメントに書いても、リスト内の確認済みの項目が普遍的な Lean の定理に変わるわけではありません。

数値的な議論では、主張に厳密性が必要なら厳密演算を使います。数値的な結論を使う前に、実際の対象／事象と有限データとの対応を証明してください。順序付きか順序なしのペアか、重複度、添字、ゼロの場合、丸めなど、重要な規約を記録してください。

仕様とプロジェクトの慣例に基づき、想定する信頼基盤について合意してください。不完全なカーネルレベルの証明を完成したように見せるために、公理やコンパイラに依存する計算を黙って導入してはいけません。一方で、あるプロジェクトで列挙や native_decide が禁止されているからといって、それを普遍的な禁止事項にしてはいけません。追加の信頼仮定があれば説明し、それがこのタスクの要件を満たすかどうかを明らかにしてください。

4. 未解決のまま残っている数学的な義務をレビューする

コアワークフローの説明に従って、A、B、C を実行します。ステージの トリガー、ソースパケット、敵対的プロンプト、異議への対応、再開、停止規則については、 references/adversarial-review.md を参照してください。これらは 数学的なチェックであり、実行者の要約を信頼するかどうかを決める投票ではありません。

既存の ARIS の証明監査／提出の役割には proof-checker を使用してください。このスキルは、 その成果物やレビュアーとの契約に取って代わるものではありません。親の 証明監査から呼び出された場合は、確認した範囲と根拠をその実行に返してください。 proof-checker を再帰的に呼び出してはいけません。Lean 単独のタスクで、 別途論文監査のワークフローが自動的に必要になるわけではありません。利用可能な場合は、 現在のホストのレビュアー振り分けに従って、対象を絞った議論と修正に research-review ／ auto-review-loop を使用してください。

モデルに直接相談する場合は、利用可能な認可済みツールと、その実際の契約を使用してください。Grok または Antigravity の MCP への相談が、自動的に ARIS のレビュアーオーバーレイとなるわけではありません。移植可能な ワークフローに、ベンダーの利用可否、クォータ、再試行回数、プロキシ設定、特定のモデルを ハードコードしないでください。

具体的な質問をしてください。この宣言を変換する、この呼び出し元の仮説を証明する、 この新しい補題に反例を見つける、この簡約の網羅性を確認する、といった質問です。生の応答、 実際に読んだ／実行した範囲、各問題に対する実行者の判断を保持してください。モデル同士の 合意は証明ではありません。同じファミリーの意見は暫定的なものにとどめ、異なるファミリーの 意見は追加のレビュー根拠であって、数学的真理の証明書ではありません。

成果物を読んでいない場合、質問への回答がない場合、呼び出しに失敗した場合、応答が空の場合は、 実質的なレビュー判定にはなりません。計画のレビューは最終コードのレビューではありません。 既存のログを読むことは、ビルドを実行することではありません。実際に確認した主張とバージョンを 記録してください。再試行は現在の認可とプロバイダーの規則の範囲内に限り、後から成功しても、 失敗を合格として書き換えてはいけません。

異議には、具体的な導出、検証済みの反例、修正、または正当化された却下をもって決着をつけてください。 未解決の議論はそのまま保持してください。呼び出した ARIS ループ独自のラウンド／継続契約を適用し、 その外側にポーリングループを作ってはいけません。直接相談の場合は、変更された義務を再レビューし、 決着がついたとき、または実際の利用可否／予算の上限に達したときに停止してください。未解決の数学的問題は 未解決のままです。依頼したレビューが利用できない場合は、保留のままです。レビュアーのスコアも ラウンドの枯渇も、証明完了の基準ではありません。

ホストでの実行とレビュー

ローカルホストの現在のモデル／推論量ポリシーとツールの契約については、レビュアーのルーティングを確認してください。このスキルの A/B/C 数学パケットを使用してください。論文、出版スコア、新しいレビュサービスは不要です。証明作業を委任する場合は、適用されるファンアウト規約に従い、安定した補題インターフェースを割り当て、各結果を実際の呼び出し元に統合してください。

Claude Code では、Lean にはホストのファイル／シェルツールを使用し、有用な並列証明作業には Agent を使用してください。デフォルトのレビュアーは Codex MCP です。mcp__codex__codex を使用し、明示的なプロジェクト cwd、読み取り専用サンドボックス、ルーティングのリファレンスから解決したモデル／推論量の組み合わせを指定して開始してください。保存されたセッション ID とプロンプトを使い、mcp__codex__codex-reply でそのレビューを続行してください。A と C では新しいコンテキストを開始してください。B の修正確認では、問題を発見したレビュアーを引き続き使用できます。このメインラインスキルを実行しているすべてのホストが Claude だと決めつけず、実行側とレビュアー側のファミリーを確認してください。

A/B/C の各チェックポイントでは、選択可能なレビュアーを通じて選択したルートを解決してください。明示的なファミリー要件を守り、満たされていないチェックポイントは保留のままにしてください。Claude、Grok、Gemini の直接トランスポートでは、ファイルアクセスと継続の契約がそれぞれ異なります。これらを使用する場合は、レビューのトランスポートに関する注意事項を確認してください。これらの Lean に関する相談によって、別のスキルのレビュアーバックエンドや受け入れルールが変更されることはありません。

5. 実際の最終ターゲットを検証する

最終ビルド、信頼性監査、またはポータブルパッケージを準備する際は、references/verification-and-handoff.md を使用してください。

納品を完了するには、該当する以下の証拠を確認してください。証明済みの定理と、未完了の再現またはレビュー要件は区別してください。

• 命題に証明があること： キーワードではなく、エクスポートされた宣言の実際の型を調べてください。theorem、lemma、または def が、対象の命題を証明する項を与えている場合があります。その命題を定義するだけ、P → P を証明するだけ、または無関係な命題を証明するだけでは、元のターゲットを満たしたことにはなりません。
• 命題の整合性： 展開された型と定義が元の主張を表していることを確認してください。元の主張に含まれていない限り、内部プロファイル、証明書の有効性、カバレッジ、成功を前提とする条件をユーザーに補わせてはなりません。
• 実際の組み立て： 簡約、場合分け、証拠、および元の結論への復帰がすべて接続され、呼び出し元からの仮定がすべて解消されていることを確認してください。
• 検証の実行： ターゲットを証明するモジュールを明示的にビルドし、その型と推移的な公理を出力してください。複数モジュールから成るプロジェクトでは、実際のエントリーポイントも独立してインポートし、エクスポートされた結果を確認してください。小規模で自己完結したファイルであれば、直接コンパイルし、型と公理を出力すれば十分です。別のインポートを作るためだけに新しいプロジェクトをビルドしないでください。コマンド、終了ステータス、出力を保存してください。別のルートモジュールのビルドが成功しても、要件を満たしたことにはなりません。
• 信頼性の計上： ターゲットの依存関係チェーンに sorryAx や未承認の追加公理がないことを確認してください。実際の依存関係を、意図された基礎と照らし合わせて説明してください。必要な一覧は、特定の公理名の固定セットと完全に一致している必要はありません。
• 再現可能性： 関連するソースと固定された環境を保持し、他の読者が実行できるコマンドを提示してください。
• 依頼されたレビュー： C は以前の計画ではなく、最終的にエクスポートされた型、定義本体、公理の出力、および元の主張を対象とします。各レビュー担当者の実質的な所見、または対応できなかった旨を個別に記録してください。

これらの確認によって、明示された基礎のもとで形式的な結果が確立されます。文章による証明や HTML 版には、それぞれ独自の対応関係の確認が必要です。Lean は、別個の解説文にあるすべての文を保証するものではありません。明示的に要求されたインポート監査、外部での再現、またはレビューは、形式的な定理の確認後も未完了のままである場合があります。そのような証拠が欠けている場合は、新たに数学的な欠陥が見つかったかのように述べず、証拠の不足として報告してください。

例示的な監査では、追加の公理なしに両方をコンパイルできる場合でも、available_interface : Target → Target と original_proof : Target を区別できます。前者では元の主張が未解決のままですが、Target がユーザーの主張と一致する場合、後者はその証明を与えます。レビュー担当者への呼び出しに失敗しても、どちらの型にも影響しません。

6. 実際に得られた証拠を保存して引き継ぐ

既存の仕様書、証明台帳、継続用ファイルを再利用します。短い進捗報告に加えて、Lean ソース、ロックファイル、監査のエントリーポイント、ログがあれば、通常は十分です。新しいファイルは、具体的な読者または実行上の必要がある場合に限って追加します。

曖昧な単一の PASS ではなく、異なる事実を報告します。

• 元の定理：確認済み、一部確認済み、主張のみ変更、または検証済みの反例により否定済みのいずれかを示し、宣言名と残っている義務を記載します。
• 命題の整合性と、実際の論理的な信頼の根拠。
• 再現状況：実際に行ったもの（既存／増分ビルド、プロジェクトのクリーンな再ビルド、または他の人による独立した再現）。
• レビュー：誰が何を読んだか、誰がコードを実行したか、依頼したレビューのうち未完了のもの。

未完了の作業については、残っている最小の数学的／Lean 上の義務、既知の依存関係、最後に役立ったエラー、次のアクションを保存します。完了した作業については、次のセッションで古い未解決事項が再び持ち出されないよう、完了したことを記録します。

2つ目の状態管理システムを作らず、簡潔な継続メモを使用します。

Original target and source:
Current exported declaration / main module:
Closed connections and actual build evidence:
Next unclosed obligation or completion:
A/B/C reviews: source scope, reviewer, raw record, remaining issue:
Next action:

「完了」または「未完了」と記した古い説明ではなく、実際の成果物から現在の状態を判断します。再開時には作業を繰り返す前に、変更点を確認します。過去と現在のレビュースコープを統合し、実際より広い監査を主張してはいけません。

研究用 Wiki を使用している場合は、既存の research-wiki／proof-checker ワークフローを通じて、正確な根拠とスコープを添えて該当する主張を更新します。生成済みのグラフを上書きしたり、別の受け入れ形式を作り出したりしてはいけません。文献検索は、数学上の未解決点、API に関する疑問、または関連する先行研究の解決に役立てるものであり、文献を網羅すること自体を無関係な要件にしてはいけません。

引き継ぎでは、読者向けの証明、ソース、固定された依存関係、独立した監査コマンド、既知の信頼境界を提供します。単一ファイルの閲覧用資料が役立つ場合は、render-html を使用します。数学的なソースを変更した場合は、適切な再ビルドと命題／公理のチェックが必要です。Markdown または HTML 内の定理や仮説を変更することも主張の変更にあたります。その場合は、整合性の確認と、依頼された関連レビューをやり直します。主張を変えないレイアウトや表現の変更には、表示の確認が必要です。変更履歴は研究記録に残し、完成した証明をそのまま提示します。ワークフロー上の形式を満たすためだけに、完了した証明作業をやり直してはいけません。