writing-lean-proofs

Lean の証明を書く

目次

• 使用する場面
• 使用しない場面
• ワークフロー
• 抽出の段階
• クイックリファレンス
• 退けるべき合理化
• 参考資料

Mathlib のスタイルとレビュー規約、および大規模な形式化プロジェクト（Liquid Tensor Experiment、PFR、Fermat's Last Theorem）の方法論から導き出した、Lean 4 の構造化された証明の記述とライブラリ設計です。

基本原則：トップダウンで設計し、ボトムアップで証明します。 Lean の命題は証明に依存しないため、後続の宣言に影響するのは定理の命題だけです。命題は安定したインターフェースであり、証明は使い捨てで自由に置き換えられます。定義と命題の設計に労力をかけ、すでにコンパイルできるスケルトン（sorryを除く）に対して証明を埋めていきます。

使用する場面

• 単一の補題から複数ファイルにまたがる開発まで、Lean 4 で定理を証明する場合
• Lean で数学、プロトコル、ソフトウェア仕様を形式化する場合
• Lean ライブラリで新しい型、構造体、関数を定義する場合
• 読みやすさ、保守性、Mathlib への適合性を考慮して Lean コードをレビューする場合
• 長いタクティク証明や壊れやすいタクティク証明を補題に分割してリファクタリングする場合
• 複数の人やエージェントが並行して貢献する形式化プロジェクトを立ち上げる場合
• Lean プロジェクトの CI、リンター、検証ゲートを設定する場合 — パターンが広まる前に、プロジェクト開始時に行ってください
• 遅い証明、maxHeartbeatsのタイムアウト、または高コストな簡約を診断する場合
• カスタムタクティク、マクロ、またはプロジェクト固有のリンターを書く場合

使用しない場面

• 汎用プログラミング言語として Lean 4 を使う場合（証明を伴わない場合）— このスキルの大半は証明と API 構造を対象としています
• Coq、Isabelle、Agda、または Lean 3 を使う場合 — 規約やタクティク名が異なります。Lean 3 の慣用表現（ge_or_gtリンティング、discrete_field）は廃れています
• 独自のコーディング規約を持つ検証済みソフトウェアの Lean プロジェクト（仕様との追跡可能性を最優先するコードベースなど）の場合：Mathlib の規約はコミュニティの標準ですが、まずプロジェクトの CONTRIBUTING を確認し、それに従ってください

ワークフロー

1. 定義とその API を先に設計する

設計の要となるのは定義です。新しい概念について何かを証明する前に、次の点を確認してください。

• 署名では部分型やOptionよりも、全域関数とダミー値を優先します（Mathlib：(0 : ℝ)⁻¹ = 0）。これにより、条件はすべての使用箇所ではなく、それを必要とする補題にだけ現れます。
• まとめます：新しい射の種類にはFunLikeインスタンスを持つ構造体を使い、新しい部分対象の種類にはSetLikeを使います。性質の証明は、個別のIsHom形式の述語ではなく、構造体のフィールドとして持たせます。
• 同値な形式が複数ある概念ごとに、正準的な表記（simpで正規化される形）を選び、その形式についてのみ API の補題を記述します。
• API は同じファイル内ですぐに記述します：定義をどこかで使う前に、ext、@[simp]、強制変換、単射性の補題を用意します。後続の証明では API を使い、unfoldやshow ... from rflは使いません。

設計規則の詳しい説明と根拠については、library-design.mdを参照してください。

2. sorry スケルトンを作る

あらゆる規模で、証明より先にすべてを記述します。

• プロジェクト規模：目標の定理と、それに必要な補題をすべて:= sorryとして記述し、ファイルがコンパイルできるようにします。これで各 sorryは独立した作業単位になります。人間や LLM の貢献者は、残りを理解しなくても一つずつ解決できます。LTE、PFR、FLT が数十人の並行貢献者によって拡大できたのは、この方法によるものです。
• 証明規模：証明の中で、sorryによる根拠を付けてhave／suffices／calcのスケルトンを組み立て、Lean がその構造を受け入れるようにしてから、各ステップを埋めます。作業中に役立つエラーメッセージが得られるのは、構造を保つからです。

example (a b c d : ℝ) (h : c = d * a + b) (h' : b = a * d) : c = 2 * a * d := by
  calc
    c = d * a + b     := sorry
    _ = d * a + a * d := sorry
    _ = 2 * a * d     := sorry

3. 目標を埋めるときは、一度に焦点を当てる目標を一つにする

• 新しい部分目標ごとに、焦点化ドット · とインデントされたブロックを付けます。焦点化されていない複数の目標を連続してアクティブなままにしないでください（Mathlib の multiGoal リンターで検出されます）。これにより、脆弱な目標の順序への依存を防げます。
• 各ブロックは、目標を明示する冗長な show で始めます。証明はこれがなくても機能しますが、レビュー担当者や将来の編集者には必要です。show によって目標が変わる場合は、代わりに change を使い、明示する目標が正確になるようにします。
• 等式や不等式の連鎖的な書き換えは calc ブロックにし、関係演算子を縦に揃えます。
• 前向きの足がかり（「まず X を確立します」）には have を、後ろ向きの簡約（「X を示せば十分です」）には suffices を使います。
• 下書き中は、明白でないタクティクの前に、目標の状態をコメントとして記録します。Lean が出力した状態を使い、想像で書かないでください。ヘッドレスのワークフローでは、確認したい箇所に trace_state を挿入するか、目標を閉じるはずの箇所に意図的に done を置いてから、lake env lean Path/To/File.lean を実行し、報告された仮定、ケース名、ゴールをコピーします。証明が機能したら、定型的な確認コードは削除します。これは LLM が作成した証明に最も効果的な手法です（llm-techniques.md を参照）。

タクティクのスタイル規則の全容については proof-style.md を、補題の内容から名前を推測できるようにする命名規則については naming-conventions.md を参照してください。

4. 機械的に検証する

スタイルを目視で確認せず、チェッカーを実行してください。lake build は最低限の基準であり、それだけでは不十分です。sorry は警告なので、ビルドが成功して終了コードが 0 でも、sorry が残っている場合があります。

• 証明されていない義務の検出には、grep ではなくカーネルを使います。 部分的な確認には #print axioms myTheorem を使います。CI では Lean.collectAxioms で宣言ごとに公理を収集し、期待される公理全体（意図的に範囲を広げない限り [propext, Classical.choice, Quot.sound]）と一致することを検証してください。そうすれば、紛れ込んだ sorry も、native_decide のような新たな信頼仮定も確実に失敗します。grep は両方の点で不適切です。コメント中の単語にも一致する一方、自身の本文には問題がなくても証明されていない補助定理を適用する定理は見逃します。動作するスクリプトは linting.md にあります。
• プロジェクトでの役割に応じてリンターを選び、プロジェクト開始時から CI に組み込みます。 下流プロジェクトで linter.mathlibStandardSet を一括で有効にしないでください。これは証明の保守性チェックに加えて、公開 API のチェック、独自のスタイル、Mathlib 固有のリポジトリ方針をまとめたものです。自己完結した証明では、まず linter.auxLemma、linter.style.maxHeartbeats、linter.style.multiGoal、linter.style.setOption、linter.style.show を有効にします。再利用可能なライブラリでは、さらに linter.flexible、linter.style.missingEnd、linter.style.openClassical、および 2 つの unused*InType チェックも有効にします。nativeDecide は信頼ポリシーの選択として扱い、フォーマットや非推奨構文のチェックはプロジェクトのスタイルとして扱います。警告でビルドを失敗させない限り、警告によってゲートされるものはありません。Batteries の宣言レベルの #lint チェック（simpNF を含む）は個別に実行します。すべてのオプションを固定バージョンの Mathlib ソースと、既知のトリガー用フィクスチャで確認してください。スペルミスのある weak. オプションは意図的に無視されます。26 項目すべての監査と lakefile のプロファイルは linting.md にあります。
• プロジェクト固有の規約（simp セットの規律、要約補題の網羅性、必須属性）ごとにカスタムリンターを作成します。 宣言レベルの @[env_linter] はそのための一つの構造であり、「30 個中 29 個の宣言で属性が欠けている」ことを確実に検出できる唯一の方法です。実装手順とエンジニアリング上の規則（空虚性のアンカー、失敗することの証明、許可リスト）については linting.md を参照してください。

抽出の段階

証明の構造は、どのような場合に独立した補題へと発展しますか？

0. 抽出する前に、断片の型を述べ、形状から検索します。 提案する命題をスクラッチの example に置き、裸のゴールに対して exact? と apply? を実行してから、型パターン検索とソース検索を試します。既存の定理が適合する場合は、それを使います。失敗した検索を記録せずに、API に不足があると報告してはいけません。

1. 1 つの証明内で部分的な議論が繰り返される → ローカルな have として名前を付けます。

   theorem min_comm (a b : ℝ) : min a b = min b a := by
     have h : ∀ x y : ℝ, min x y ≤ min y x := by
       intro x y
       apply le_min
       · show min x y ≤ y
         exact min_le_right x y
       · show min x y ≤ x
         exact min_le_left x y
     apply le_antisymm
     · show min a b ≤ min b a
       exact h a b
     · show min b a ≤ min a b
       exact h b a
   

2. 命題自体に独立した意義がある、または抽出によって部分的な議論に不要な仮定を取り除ける → 独立した補題にします。不要な仮定を取り除けることは、より強い判断基準です。抽出した補題は、元の証明よりも一般的になります。

3. 証明が「長く扱いにくい」と感じられる → 分割します。これは Mathlib のレビュー基準であり、意図的に定性的なものです。行数の基準はありません。迷ったら、抽出を試してください。断片に明確な命題を付けられるなら、補題にするべきです。

クイックリファレンス

ルール	理由	強制方法
後続の箇所で定義を展開しない。erw または末尾の rfl は API 不足の兆候です	API 補題は抽象化の境界です	レビュー（「API 不足」の兆候）
末尾の simp は簡約した形のままにします。末尾以外の simp は simp only [...] にします	簡約した末尾の呼び出しは重要な補題を埋もれさせ、名前の変更で壊れます	スタイルガイド
一度に扱うゴールは 1 つにします（· ブロック）	ゴールの順序に依存する脆さをなくします	linter.style.multiGoal
show でゴールを変更してはいけません（change を使います）	明示したゴールの正確さを保ちます	linter.style.show
最終コードに set_option によるデバッグ、トレース、プロファイラーの設定や、スコープ外の maxHeartbeats を残しません	デバッグ用の足場です	linter.style.setOption
補題は simp 正規形で記述し、> ではなく < を使います	simp は構文に基づいて照合します	simpNF リンター
短縮は、結果が少なくとも同程度に読みやすい場合に限ります。自明な結果は例外です	短いことと良いことは同じではありません	レビュー
Fact インスタンスはローカルにし、グローバルにしません	グローバルインスタンスは、すべての型クラス検索の性能を低下させます	レビュー
補題の名前は命題に基づいて付けます（命名リファレンスを参照）	検索しなくても名前から推測できるようになります	linter.style.nameCheck が検出するのは __ のみです。#lint defsWithUnderscore とレビューでさらに確認します
補助定理を書いたり API 不足を主張したりする前に、裸のゴールを形状から検索します	目標から名前を常に推測できるとは限りません	exact?、apply?、型／ソース検索
原則として、1 行に tactic の呼び出しを 1 つだけ置きます。1 行で閉じる証明は例外です	絶対的なルールを設けることなく、読みやすい証明構造を保ちます	スタイルガイド
sorry は collectAxioms／#print axioms で検査し、grep は使いません	grep はコメントに一致する一方、未証明の補助定理を見落とします	CI での公理監査
simp 補題の左辺は数値ではなく構造に基づくものを優先し、定数ごとに表記を 1 つに統一します	2 ^ 32 は、4294967296 に正規化されたゴールとは一致しません	simpNF、レビュー
すべての simp only リストは、それぞれの箇所で simp? を使って導き直します	見た目が似たゴールでも、リストを使い回せるとは限りません	linter.flexible
maxHeartbeats の上書きはすべて、証明されていない主張です。信じる前に計測します	コピーされた予算には情報がありません	#count_heartbeats、二分探索
条件付き simp 補題が浅い箇所では適用されるのに、深い箇所では適用されない → maxDischargeDepth（デフォルトは 2）を引き上げます	連鎖する副条件は診断なしに途中で打ち切られます	診断（証明スタイル、simp の規律）
プロジェクト固有の慣習にはすべてカスタムリンターを用意し、初日から CI に組み込みます	レビューでは、30 件中 29 件が失敗するケースを見落とします	@[env_linter] ＋ #lint

各行の詳しい理由と、ライブラリレベルのアンチパターンについては、 anti-patterns.md を参照してください。

却下すべき合理化

言い訳	実情
「証明がコンパイルできる。これで出そう」	コンパイルできることは最低条件です。Lean だけが読める巨大な tactic ブロックは、次の Mathlib の更新で気づかないうちに壊れ、誰も修復できなくなります。
「API の補題を書くより、定義を展開するほうが簡単だ」	後続のあらゆる unfold が、証明を実装に結び付けます。最初のリファクタリングで、すべてが一度に壊れます。不足している補題を書きましょう。
「simp をすべて絞り込めば、証明が速くなり、堅牢性も増す」	最後に実行する simp 呼び出しでは逆効果です。絞り込んだリストは名前変更のたびに壊れ、重要な情報を埋もれさせます。絞り込むのは最後ではない呼び出しだけにしましょう。
「短いほうが優れている」	Mathlib のレビュー方針では、可読性を損なわない場合に限り、ゴルフは問題ありません。目指すべきは短さではなく、読みやすさです。
「動作してから補題に整理し直そう」	動作するようになった後では、その構造が不可欠になり、複雑に絡み合っています。まず骨格を記述すれば、補題は自然に導かれます。
「show 行を追加しても冗長なノイズだ」	カーネルにとっては冗長ですが、次に証明を読む人間やモデルにとっては不可欠です。
「このヘルパーは補題にするには具体的すぎる」	明確な命題として記述できるなら、切り出しましょう。不要な仮定を取り除くと、最初から一般的な補題だったと分かることがよくあります。
「ライブラリが安定したらリンターを追加しよう」	逆です。パターンはコピー＆ペーストで広がるため、リンターを先送りすると、たった一行の問題ではなく、400 件の警告に対処することになります。すでに問題のない項目は今すぐ有効にして、ゲートを設けましょう。
「チェックに通ったから、問題はない」	失敗できないチェックは何も証明しません。全ファイルを対象にするはずのチェックが対象をゼロ件にしたり、スペルミスのある weak. オプションが無視されたり、パイプラインが終了コードを握りつぶしたりします。チェックに通ったと信頼する前に、各ゲートが失敗することを確認してください。
「証明に時間がかかるから、maxHeartbeats を増やそう」	測定されていない予算は主張であって、修正ではありません。そして、次の読者が気づくべき性能低下を覆い隠してしまいます。#count_heartbeats で測定し、定義を再構成するか、ゴールを分解しましょう。

参考資料

• library-design.md — 定義、API、 バンドル化、抽象化の境界、仕様主導のプロジェクト分解
• proof-style.md — tactic による証明の構成： calc、have/suffices、焦点化、simp の規律、および 補題が発火しない理由の診断（適用の深さ、走査順序、 数値の表記法）
• naming-conventions.md — 命題から補題名を算出できるようにする Mathlib の命名規則
• anti-patterns.md — 認識されているアンチパターン、 それぞれが有害な理由、および検出するリンター
• llm-techniques.md — LLM が記述する証明に特化した、 エビデンスに基づく手法
• linting.md — 公理に基づく sorry ゲート、CI で早期に プロジェクト固有のリンタープロファイルを有効にする方法、Mathlib 標準セット全体の 監査、未解消の警告がある状態でのリンター導入、プロジェクト固有の構文を対象とする カスタムリンターの作成、およびすべてのゲートが失敗できることの確認
• performance.md — 宣言ごとのコストの測定方法、 簡約コストの発生源、意味を損なわずに定義を最適化する方法
• tactics.md — メタプログラミングの規律： 拡張ポイントの選択、メタ変数と復旧のための安全策、探索範囲の制限、 実行可能なエラーメッセージ、構造化トレース、生成される宣言、 および失敗条件のテスト