proof-writer

Proof Write：厳密な定理／補題の草稿作成

見栄えだけの偽の証明ではなく、数学的に誠実な証明パッケージを作成してください。

定数

• DEFAULT_PROOF_DOC = プロジェクトルートの PROOF_PACKAGE.md
• STATUS = PROVABLE AS STATED | PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION | NOT CURRENTLY JUSTIFIED

コンテキスト：$ARGUMENTS

目標

次のうち、必ず1つだけを作成してください。

1. 元の主張の完全な証明
2. 修正した主張と、その修正後の主張の証明
3. 主張が現時点では正当化できない理由を説明する、証明が行き詰まっている旨の報告

入力

次の項目を抽出し、整理してください。

• 定理／補題／命題／系の正確な記述
• 明示的な仮定
• 記法と定義
• ユーザーが提示した証明の概略、部分的な証明、または意図する方針
• 依頼で参照されている場合は、ローカルノート、付録ファイル、定理の草稿にある関連する補題や主張
• 指定されている場合は、希望する出力スタイル（簡潔、付録向け、詳細版）

記法または仮定が曖昧な場合は、証明を始める前に、採用する解釈を明記してください。

ワークフロー

ステップ1：証明に必要なコンテキストを収集する

次の優先順位で、対象となる証明ファイルを特定してください。

1. ユーザーが明示的に指定したファイルパス
2. ローカルノートまたは定理ファイルですでに参照されている証明の草稿
3. 既定の対象ファイルであるプロジェクトルートの PROOF_PACKAGE.md

関連するローカルコンテキストを読み取ってください。

• 選択した対象の証明ファイル（すでに存在する場合）
• 定理のノート、付録の草稿、またはユーザーが明示的に言及したファイル

次の項目を抽出してください。

• 正確な主張
• 仮定
• 記法
• 証明の概略または部分的な証明
• 草稿が依拠する可能性のある関連補題

ステップ2：主張を整理する

次の内容を明確に述べてください。

• 証明する正確な主張
• 結論とは分けて示した、すべての仮定
• 主張で使われているすべての記号

次の点を特定してください。

• 隠れた仮定
• 未定義の記法
• 対象範囲の曖昧さ
• 利用可能な証明の概略が完全な主張を証明しているのか、それともより弱い変形だけを証明しているのか

ユーザーの元の定理の記述は、変更が明示的に必要な場合を除き、そのまま維持してください。 証明を容易にするためだけに、より強い形への整理や、より簡潔な内部表現を使う場合は、それを内部的な証明上の手段として扱い、元の主張を暗黙に置き換えないでください。

Lean による証明を選ぶ場合

ユーザーが Lean を指定した場合、または特定の証明義務を形式化することで正しさを大きく確かめられる場合は、元の記述、現在の試み、既知の依存関係を添えて /lean-formalize を呼び出してください。このスキルでは、証明とその形式的な実装の両方を作成します。検証済みの範囲、エクスポートされた定理、残る証明義務をこの証明パッケージに返してください。部分的な結果で解消されるのは、対応する証明義務だけです。不足している数学的議論の作成のために lean-formalize から呼び出された場合は、その議論と残る不足箇所を呼び出し元の Lean 実行に返し、lean-formalize を再帰的に呼び出さないでください。通常の証明草稿の作成に Lean は必要ありません。難しいというだけでは、Lean を使う理由になりません。

ステップ3：実現可能性を判定する

証明を書く前に、主張を次のステータスのうち、必ず1つに分類してください。

• PROVABLE AS STATED
• PROVABLE AFTER WEAKENING / EXTRA ASSUMPTION
• NOT CURRENTLY JUSTIFIED

次の点を明示的に確認してください。

• 結論は、列挙された仮定から実際に導かれるか
• 引用された定理が、その条件を満たさない形で使われていないか
• 主張が、利用可能な議論で裏付けられる範囲を超えていないか
• 明白な反例、境界事例、または量化の不備がないか

主張が記述どおりには証明できない場合、証明を捏造してはいけません。 証明を成立させるためだけに、仮定を暗黙に強めたり、定理の対象範囲を狭めたりしてはいけません。

Step 4: 依存関係マップを作成する

証明方針を選びます。たとえば、次のような方法があります。

• 直接証明
• 背理法
• 帰納法
• 構成法
• 既知の結果への帰着
• カップリング／確率論的議論
• 最適化不等式の連鎖

次に、依存関係マップを作成します。

• 主張
• 必要な中間補題
• 引用する定理や不等式の名称
• 各自明でないステップが依存する仮定
• 個別に扱う必要がある境界ケース

ステップが複雑な場合は、1文に埋め込まず、補題として切り分けます。

Step 5: 証明ドキュメントを作成する

選択した対象の証明ファイルに書き込みます。

対象の証明ファイルがすでに存在する場合：

• まず読みます
• 該当する主張のセクションを更新します
• 既存の内容をむやみに重複させません

ユーザーが対象を指定しない場合は、プロジェクトのルートにある PROOF_PACKAGE.md を既定のファイルとします。

ユーザーがその対象を明示的に指定しない限り、論文のセクションや付録の .tex ファイルに直接書き込まないでください。

証明パッケージには、次の項目を含める必要があります。

• 正確な主張
• 明示的な仮定
• 証明のステータス
• 宣言した方針
• 依存関係マップ
• 番号付きの主要なステップ
• 自明でないすべての含意の根拠

数学的厳密さの要件：

• 論理の飛躍を隠すために、「明らかに」「自明に」「示すことができる」「標準的な議論により」「同様に」を決して使わないでください
• すべての定数と記号を、使用する前に定義してください
• 量化子の順序を注意深く確認してください
• 退化ケースと境界ケースを明示的に扱うか、除外される理由を述べてください
• 標準的な事実を使う場合は、その名称と、ここでその仮定が満たされる理由を述べてください
• インライン数式には $...$、ディスプレイ数式には $$...$$ を使ってください
• 数式をプレーンテキストで書かないでください
• 証明でユーザーの元の定理文より強く見える同値な正規化を使う場合は、それが証明上の便宜であることを明記し、元の主張とは分けてください

Step 6: 最終確認

対象の証明ファイルを仕上げる前に、次の点を確認してください。

• 定理の記述が、実際に示された内容と正確に一致している
• 使用したすべての仮定が記載されている
• 自明でないすべての含意に根拠がある
• すべての不等式の向きが正しい
• 引用した結果が、記載された仮定のもとで適用可能である
• 端点ケースが扱われているか、明示的に除外されている
• 未証明の補題に依存する隠れた箇所がない

重要なステップにまだ根拠がない場合は、無理に証明せず、ステータスを引き下げて問題点を報告してください。

必須のファイル構成

次の構成で対象の証明ファイルを作成してください。

# Proof Package

## Claim
[exact statement]

## Status
PROVABLE AS STATED / PROVABLE AFTER WEAKENING / NOT CURRENTLY JUSTIFIED

## Assumptions
- ...

## Notation
- ...

## Proof Strategy
[chosen approach and why]

## Dependency Map
1. Main claim depends on ...
2. Lemma A depends on ...
3. Step k uses ...

## Proof
Step 1. ...
Step 2. ...
...
Therefore the claim follows. ∎

## Corrections or Missing Assumptions
- [only if needed]

## Open Risks
- [remaining fragile points, if any]

応答モード

主張がそのまま証明できる場合

完全な証明を含め、上記のファイル構成に沿ったファイル全体を作成してください。

元の主張が強すぎる場合

次の内容を記載してください。

• 元の主張が正当化できない理由
• 修正した主張
• 追加の仮定があれば、そのうち必要最小限のもの
• 修正した主張の証明

誠実に証明を完了できない場合

次の内容を記載してください。

• Status: NOT CURRENTLY JUSTIFIED
• 正確な問題点：欠落している補題、無効な含意、隠れた仮定、または反例の方向性
• 証明を完了するために必要な追加の仮定、補題、または導出
• 可能であれば、より弱い修正済みの主張

チャットでの応答

対象の証明ファイルを書き込んだ後、次の内容を簡潔に応答してください。

• ステータス
• 元の主張が変更なく維持されたかどうか
• 更新したファイル

重要なルール

• 欠落している証明ステップを決して捏造しないでください。
• 主張を誇張するより、弱めることを優先してください。
• 仮定、導出された事実、ヒューリスティクス、予想を区別してください。
• 修正した主張や内部的な正規化として明示しない限り、ユーザーの元の定理の記述を維持してください。
• 記述がそのままでは誤りの場合は、そう明言し、反例または修正した主張を示してください。
• 不確実性が残る場合は、Open Risks に明記し、整った文章の中に隠さないでください。
• 簡潔さより正確さを優先してください。