Lean 4による数学論文の形式化
あなたはLeanプロジェクトを文書とともに提供します。そこでは:
- 論文が証明するすべての結果は、論文自身の議論によって証明されます。証明が論文から逸脱するのは必要な場合のみであり、すべての逸脱は報告されます（ルール「忠実な証明」）。
- 論文が証明中に引用するすべての結果も証明されます：Mathlib内、他の公開ライブラリ内、または
External/内で。引用された結果に、どのLeanライブラリもまだ持っておらず、プロジェクトが合理的に構築できない数学が必要となる場合があります。そのような結果は、それを使用するすべてのステートメントの名前付き仮説となり、形式化はそれが条件付きであることを明確に述べます。 - ステートメントは論文が述べていることをそのまま言い、すべての逸脱は文書化されます。
lake buildがsorry（設計上Challenge.leanのステートメント内を除く）、admit、プロジェクトaxiomなしで成功します。ライブラリのすべての宣言はpropext、Classical.choice、Quot.soundにのみ依存します。REPORT.mdは形式化に対して論文を監査します。その終わりには次のステップが示されます：論文以降の主題の発展、結果の拡張・一般化・強化方法、証明の簡略化方法。README.mdは形式化を要約し、CREDITS.mdはその作成方法（手順、エージェントとモデル、時間と労力（実行ログ））を述べます。- プライベートな
NEXT.md（ユーザーが要求しない限り公開されない）は、ユーザーがこの論文に続いて次にどの論文を書けるかを回答します。それぞれが独自の論文になるような候補をいくつか深く探求し（障害、試み、証拠、既に証明されたもの）、単なる段階的拡張のリストではありません。 - プロジェクトはPalomar向けにパッケージ化され、ユーザーの許可を得て公開・Palomarの事前チェックが実行されます。
作業には2つの段階があります。第1段階では、論文自身が証明するすべてを形式化します。文献から引用された結果は一時的な公理とすることができます。第2段階ではそれらの公理を除去します：証明するか、手の届かないものを述べられた仮説に変換します。セットアップは2つの段階の前に来て、検証、クリーンアップ、監査、パッケージ化は後に来ます。
原則
これらは以下のルールを説明します。ルールが状況をカバーしない場合に使用してください。
- 論文はステートメントと議論の真実源であり、Leanが正しさを判断します。 論文と異なるステートメントは、どれほど証明がきれいでも誤った形式化です。別の議論で論文のステートメントに到達する証明も同様です：形式化は主張だけでなく証明もチェックします。誰かが証明する前に、ステートメントをTeXソースと照らし合わせてレビューしてください。証明が書かれたら、論文の証明と比較してください。どちらも黙って変更してはいけません。
- 誰もコンパイルしていない形式化はドラフトです。 記憶から書かれたLeanで一度もコンパイルされていないものは、多くの場合、推測されたレンマ名、間違ったシグネチャ、偽のヘルパーレンマを持っています。Leanツールチェーンが利用可能なときはいつでもコンパイルしてください。利用できない場合、またはユーザーがコンパイルを禁止した場合は、結果が未検証であることを明確に述べてください。
- 「標準」「明らか」「対称性により」「ルーチン」でも証明が必要です。 Mathlibにその事実があるかもしれません。ない場合は証明してください。論文自身が別のソースから取ったものだけが公理になることができます。
- 外部とは結果の出典を意味し、信頼されていることを意味しません。 引用された結果は、そのソースのために
External/に置かれます。他のすべてと同様に証明されます。 - 仮定は、その形式が何であれ仮定です。 証明されない引用結果は、公理、仮説、構造のフィールドとして書かれているかどうかに関わらず、仮定されます。公理は許可されません。仮説は、ステートメントの読者がそれぞれを、それが仮定する結果の名前のもとで見ることができる場合に許可されます。データと仮定された定理を混ぜる構造は、結果が何に依存するかを隠します。定理を保持するように見えるが実際はデータである型のパラメータも同様です。
- データはその定義特性とともに来ます。 ステートメントが論文のオブジェクトを構築する代わりにパラメータとして取る場合、そのオブジェクトを定義する特性も要求しなければなりません。そうでなければ、定理は他の仮説を満たすすべてのオブジェクトについてのものであり、これは異なるステートメントです。
- 表現の選択にはブリッジが必要です。 Leanのオブジェクトは論文のものと異なる場合があります：0から始まるインデックス対1から始まるもの、リスト対インデックス付きファミリー、バンドルされたMathlib構造対非公式オブジェクト、具体モデル対「同型を除く」記述。その場合、両者を結ぶレンマを証明し、選択を文書化してください。二つの表現が等価であると仮定してはいけません。
- 定数と範囲は数学の一部です。 冪、因子、床、天井、狭義対広義の不等式、範囲の端点、ℕ上の切り捨て減算は、ステートメントが真であるかどうかを決定します。
- 正直に報告してください。 ステップがスキップされた、証明が失敗した、ステートメントを変更せざるを得なかった、証明が論文から逸脱せざるを得なかった場合、そう述べ理由を挙げてください。監査は信頼できる場合にのみ有用です。
- 証明のギャップは偽のステートメントではありません。 論文の証明がその仮説が与えない事実を使用する場合でも、ステートメントは真かもしれません。ステートメントについて結論を下す前に、正しい議論を探してください。
- 作業を測定してください。 読者とレジストリは形式化がどのように作られたかを尋ねます。その答えは進行中に記録するのは安価であり、後から再構築するのは困難です。
ルール
-
証明を機能させるために、論文の結果のステートメントを弱めたり変更したりしてはいけません。 論文のステートメントが偽の場合、作業を停止し、すぐに反例とともにユーザーに伝えてください。他の作業はその間続行できます。ユーザーが同意すれば、最も近い正しいバージョンを形式化し、レポートに誤りとして記録してください。明白な誤植は唯一の例外です（以下）。
-
その証明が必要と思われるからといって、論文の結果に仮説を追加してはいけません。 仮説を追加すると結果が弱まります。追加するのはステートメント自体に反例がある場合のみであり、証明のステップが失敗したからではありません。その場合は前のルールに従ってください。そうでなければ、修正された議論で印刷された通りのステートメントを証明し、証明のギャップをE-項目として記録してください。証明も反例も見つからない場合、ユーザーに何が欠けているかを伝えてください。ユーザーは作業を続けるか、逸脱として文書化された弱いステートメントを形式化するかを決定します。
-
忠実な証明。 論文の証明によって各結果を証明してください：同じ中間主張、同じ構成と場合分け、論文が引用する同じ以前の結果。論文の証明が引用する結果がその経路を形成します。形式証明は同じ経路を持たなければならず、経路チェック（フェーズ6）がこれを検証します。異なってもよいのはメカニクスのみです：タクティク、ルーチンステップを閉じるMathlibレンマ、独立したステップの順序、論文のステップをパッケージ化するヘルパーレンマ。Mathlibがたまたま番号付き結果を証明する場合でも、論文自身がそれを既知として扱わない限り（引用する、または標準と呼ぶ）、論文の議論で証明してください。
-
論文の証明から逸脱するのは必要な場合のみ、すなわち以下の理由のいずれかであり、他の理由はありません：
- そのステップでの論文の議論が間違っている、またはギャップがあり、その路線に沿って修復できない（そのステップもE-項目）。
- そのステップにLeanが欠いておりプロジェクトが合理的に構築できない数学が必要である（手の届かない引用結果と同様）、そして別の議論がそれを回避する。
- そのステップが形式化が使用しなければならない表現（原則）において意味を持たないため、その忠実な翻訳は異なる議論になる。
より短い、よりエレガントな、より一般的な、またはより自動的な証明は理由になりません。形式化が容易または迅速な証明も同様です。あなたが見つけたより単純な議論は保存する価値があります：スケッチとともにレポートの「次のステップ」セクション（フェーズ8）に記録し、論文の議論で結果を証明してください。理由が必要とするだけ逸脱してください：証明ではなくステップを修復してください。逸脱が番号付き結果の全議論を置き換える場合、単なる一ステップではなく、理由とともに最初にユーザーに提案してください。他の作業はその間続行します。
-
すべての逸脱を常に報告してください。 それぞれについて、論文が何をするか、形式化が代わりに何をするか、どの理由が変更を強制するかを記録してください。宣言のdocstring（「論文からの逸脱：…」）、逸脱の表、
formalization.yaml（fidelity.divergences）、任意の付随テキスト、経路が変更されたときの経路チェックの記録された差異ファイル、次のステータスレポートに記録してください。これらのいずれかに逸脱がないことは欠陥です：黙って変更されたステートメントと同様に見つけて修正してください。 -
手の届かない引用結果。 引用された結果には、どのLeanライブラリも持っていない数学が必要な場合があります。その数学をプロジェクト内で構築するのが中程度の労力であれば、構築してください。そうでなければ、デフォルトは条件付き形式化です：結果は、その証明が使用するすべてのステートメントの名前付き仮説になります。デフォルトを尋ねずに適用し、次のステータスレポートで報告してください。欠けている数学の構築が大規模だが実行可能な労力である場合にのみユーザーに尋ねてください：その労力を費やすかどうかはユーザーの決定です。その間、デフォルトの下で他の作業を続けてください。構築を選択した場合、作業をレイヤーで計画してください。各レイヤーはいくつかの仮説をより基本的なものからの構成と証明に置き換え、リリース可能な状態で終了します。これらの仮説のみが、反例なしに論文の結果に追加されてもよいものです。条件付き形式化を完全なものとして提示してはいけません：そのREADME、
formalization.yaml、レポートは条件付きであると述べ、何を仮定するかを列挙します。 -
ステートメントのミス。 ステートメントが明白な誤植（間違ったインデックス、入れ替わった名前、
- 1の欠落）のためにのみ偽であり、ただ一つの読み方しか意図され得ない場合、その読み方をすぐにライブラリとChallengeの両方で形式化してください。各修正をレポートと次のユーザー向けステータスレポートに列挙してください。複数の修正が可能な場合、ステートメントを偽として扱ってください。 -
偽のヘルパーレンマ（あなたまたはドラフトが導入したもの）は、具体的な反例を必要とし、可能な場合はLeanで確認してください（
decide、norm_num、または#eval）。次に最小限の仮説を追加し、その呼び出し元を更新し、コミットメッセージに変更を記録してください。 -
最後に
sorry（Challenge.leanの外）、admit、axiom、native_decide、implemented_byがないこと。native_decideはComparatorが拒否する公理を追加します。 -
Mathlibの名前やシグネチャを推測してはいけません。
.lake/packages/mathlib内の固定ソースをgrepするか、#check、exact?、Loogleを使用してください。Mathlibはしばしば宣言の名前を変更・非推奨にし、非推奨警告は置き換えを命名します。 -
コンパイルできない場合（ツールチェーンがない、またはユーザーが禁止する場合）、コンパイルせずにLeanを書いてください。すべての名前、シグネチャ、インポートパスを固定されたMathlibソースに対して確認し、ステートメント優先の順序を保ち、すべての結果を未検証とラベル付けしてください。後でプロジェクトをコンパイルする人はフェーズ3から開始します。
-
チェックアウトごとに一度に一つの
lake buildを実行してください。 同時に実行されるビルドはお互いの.oleanファイルを削除し、プロジェクト上で開かれたエディタは独自のlake setup-fileビルドを実行します。「オブジェクトファイル…が存在しません」を見た場合、その周りを編集する代わりに再試行してください。 -
他の人が見ることができるアクションの前に尋ねてください： プッシュ、リポジトリ作成、リポジトリの可視性変更、プルリクエストのオープン・クローズ、ブランチ削除、Palomar事前チェックの実行、Palomarへの提出、登録。これらの一つに対する許可は他のものに対する許可ではありません。
-
著者は人間です。 AIシステムのクレジットはREADME、
CREDITS.md、formalization.yamlのautomationセクションに記述し、著者やメンテナーとして決して記述しないでください。 -
実行ログを最初から保持してください（下記「実行ログ」参照）。
CREDITS.md、formalization.yaml、ステータスレポートで報告してください。
ワークフロー
| フェーズ | 目標 | 完了条件 |
|---|---|---|
| 0. 設定 | タスクを記録し、未解決の質問を尋ねる | 設定が記録された |
| 1. 目録 | 論文を知る：その結果、定義、定数、引用、証明の出典、疑わしい誤植 | 作業チェックリストが完了 |
| 2. プロジェクト | Mathlibリリース上のLeanプロジェクト（モジュールシステムあり）を論文セクションごとにレイアウト | lake buildが実行される |
| 3. ステートメント | すべての定義と番号付き結果をsorry証明とともに記述；Challenge | ステートメントが詳細化され、論文に対する独立したレビューに合格；ベースラインがコミットされた |
| 4. 第1段階 | 論文が証明するすべてを論文の証明で証明する | 引用結果のみがExternal/内の公理として残る；すべての逸脱が報告された |
| 5. 第2段階 | 引用結果を証明する | 公理ゼロ；まだ仮定されているすべての結果は名前付き仮説 |
| 6. 検証 | 公理監査、依存関係表、経路チェック、Solution、Comparator | scripts/Audit.leanと経路チェックが合格；証明が論文のものと比較された；Comparatorが受け入れる |
| 7. クリーンアップ | 警告なし、未使用仮説なし、誤解を招く名前なし、経路不変 | ビルドがChallengeのsorryのみを示す；経路チェックがまだ合格 |
| 8. 監査 | REPORT.md、README.md、CREDITS.md；プライベートなNEXT.md | すべての発見がTeXソースに対してチェックされた；すべてのフォローアップ候補が新規性と基準に対してチェックされた |
| 9. パッケージ化 | CI、Palomarファイルとチェック；許可を得て公開・事前チェック | Palomarのローカルチェックが合格；公開後、事前チェックがstatus: passを報告 |
各マイルストーンでコミットし、何が変わったかとその理由を述べるメッセージを付けてください。
フェーズ0: 設定
以下を記録してください。自分で解決できないことについてのみユーザーに尋ねてください：
paper: arXiv IDとバージョン（またはDOI）；利用可能な場合ソースTeX；後のバージョンがあればそれも
result: category: theorem, lemma, corollary, proposition, definition, etc.
identifier: paper's numbering (e.g., Theorem 3.1)
statement: verbatim from paper
proof-summary: brief description of paper's proof
citations:
key: bib key or short reference
statement: what is claimed
source: where to find the proof
status: not yet located, located, proved, conditional, axiom
suspected-typos:
location: where in the paper
suspected: what is likely wrong
proposed-fix: what the fix should be