lean4

Lean 4 の定理証明

Lean 4 の証明を編集するとき、Lean のビルドをデバッグするとき、Lean で数学を形式化するとき、または Lean 4 の概念を学ぶときは、このスキルを使用してください。LSP による調査と mathlib の検索を優先し、sorry の分析、公理のチェック、エラーの解析にはスクリプト化されたプリミティブを使用します。

基本原則

証明する前に検索してください。 多くの数学的事実は mathlib にすでに存在します。タクティクを書く前に徹底的に検索してください。

段階的にビルドしてください。 Lean の型チェッカーがテストスイートになります。sorry がなく、標準の公理だけでコンパイルできれば、証明は健全です。

スコープを守ってください。 ユーザーの希望に従ってください。1 つの sorry、その推移的な依存関係、ファイル内のすべての sorry、またはすべてを埋めます。不明な場合は確認してください。

Lean ファイルでは、行の長さを 100 文字にしてください。 行を 80 文字で折り返さないでください。Lean と mathlib の慣例は 100 文字です。行が 100 文字以内に収まる場合は、1 行に保ってください。100 文字を超える行の改行方法については、mathlib-style を参照してください。

mathlib のスタイル簡易チェック。 通常の数学的なラムダには、fun x => ... ではなく fun x ↦ ...（\mapsto）を使ってください。match／do の分岐とメタプログラミングのコールバックイディオムには => を使ってください。タクティクによる証明には show P by tac を優先し、項による証明にのみ show P from term を使ってください。mathlib-style を参照してください。

命題とシグネチャを維持してください。これらはファイルの契約です。 ユーザーが明示的に変更を求めない限り、定理／補題の命題と型シグネチャは変更できません。これらを変更すると、呼び出し元に影響したり、証明対象の定理が変わったりすることがあります。命題の変更や独自の公理の追加が必要と思われる場合は、契約または証明の信頼基盤が変わるため、作業を中断してまず相談してください。例外：合成ラッパー（/lean4:formalize、/lean4:autoformalize）内では、外側のループにおける命題安全性のルールに従って、セッションで生成された宣言を再草稿できます。cycle-engine.md を参照してください。

ドックストリングの扱いはワークフローごとに異なります。 既存のドックストリングは API です。既存の宣言を変更するワークフローでは、ユーザーが明示的にドックストリングの変更を求めない限り、デフォルトで ルール A に従ってください。

モード	実行できること	境界
A — 既存の宣言の編集（例：/lean4:prove、sorry-filler-deep、ゴルフ、リファクタリング、既存の宣言を編集するあらゆるエージェント）	証明本体内のインラインコメントを調整する	既存のドックストリングは書き換えない。ユーザーから明示的な依頼があった場合のみ
B — レビュー（/lean4:review）	弱い／欠落したドックストリングを指摘し、レポート内で置き換えテキストを提案する	読み取り専用。ファイルを変更しない
C — 新規ファイル／新規宣言の生成（/lean4:draft、/lean4:formalize、/lean4:autoformalize）	新たに作成するファイルや宣言にモジュール／宣言のドックストリングを追加する	既存のドックストリングにはルール A を適用する

コマンドごとの方針は各コマンドのドキュメントに記載されています。ドックストリングに関する区分は、すべてのプロジェクトで適用されます。mathlib の Template Gate が mathlib ヘッダーを選択した場合、ルール C はそのモジュールドックストリング用のスロットを埋めます。ルール C は、テンプレートを選択したり再定義したりするものではありません。

コマンド

コマンド	用途
/lean4:draft	形式的でない主張から Lean の宣言スケルトンを作成します
/lean4:formalize	対話形式の形式化 — 下書き作成とガイド付き証明を行います
/lean4:autoformalize	形式的でないソースから、最初から最後まで自律的に形式化します
/lean4:prove	明示的なチェックポイントを設けて、サイクルごとにガイド付きで定理を証明します
/lean4:autoprove	明示的な停止予算を設けて、複数サイクルにわたり自律的に定理を証明します
/lean4:disprove	認定された反証を伴う、ガイド付きの反例探索を行います
/lean4:checkpoint	安全なコミットチェックポイントを作成して進捗を保存します
/lean4:review	Lean の証明を読み取り専用でコードレビューします
/lean4:refactor	mathlib を活用し、補助定理を抽出して、証明戦略を簡素化します
/lean4:golf	直接性、明瞭さ、パフォーマンス、簡潔さを高めるために Lean の証明を改善します
/lean4:learn	対話形式の学習と mathlib の探索を行います
/lean4:diagnose	診断、クリーンアップ、移行を支援します

/lean4:* はネイティブプラグインのコマンドエイリアスであり、このドキュメント全体で安定したワークフロー名としても使用されます。コマンド登録のないホスト（スキルのみのインストールやポータブルインストール）では、ホスト標準の構文で lean4 スキルを呼び出し、名前付きワークフローを指定してください。たとえば、「Foo.lean:42 に対してガイド付きの prove ワークフローを使用してください」と指定します。

このプラグインには、ホストに依存しないパーサー（lib/command_args/）が付属しており、パラメーターの多い7つのコマンド（draft、learn、formalize、autoformalize、prove、autoprove、disprove）について、パーサーで判定可能な起動ルールを適用します。これらのコマンドに記載されている起動ルールの一部は実行時のコンテキスト（リポジトリレベルの検索や対話形式のプロンプト）に依存するため、パーサーの出力を読み取った後にコマンド側で適用します。他のコマンド（checkpoint、review、refactor、golf、diagnose）は、引き続きモデルによってパースされます。 ホストアダプターが UserPromptSubmit フックをインストールしている場合、対象となる7つのコマンドのいずれかに一致する /lean4:* プロンプトがモデルに渡される前にパーサーが実行され、validated-invocation ブロックがコンテキストに挿入されます。また、無効な呼び出しはフックの段階で拒否されます。他のコマンドの呼び出しは変更されずに通過します。フックのないホストでは、共通の command-invocation.md コントラクトに従い、起動時のパースをモデルが行います。 コマンドは常に解決済みの入力を通知し、無効な起動設定は作業を始める前に拒否します。また、--max-total-runtime のような実時間の予算はベストエフォートとして扱います。

どのコマンドを使うべきですか？

状況	コマンド
Lean のスケルトンを作成する（デフォルトではスケルトンのみ）	/lean4:draft
下書きを作成して対話形式で証明する	/lean4:formalize
sorry を埋める（対話形式）	/lean4:prove
sorry を埋める（無人実行）	/lean4:autoprove
主張を反証するための反例を探す	/lean4:disprove
セーブポイントを作成する（ファイルごとのビルド＋プロジェクトビルド、ベストエフォートの公理スキャン、コミット）	/lean4:checkpoint
品質チェック（読み取り専用）	/lean4:review
証明戦略を簡素化する（mathlib の活用、補助定理）	/lean4:refactor
コンパイル済みの証明を最適化する	/lean4:golf
このプロジェクトを初めて使う／探索する	/lean4:learn --mode=repo
トピックに関する mathlib の情報を調べる	/lean4:learn --mode=mathlib
うまく動作しない場合	/lean4:diagnose
形式化と証明を最初から最後まで行う（無人実行）	/lean4:autoformalize --source=... --claim-select=first --out=...

貢献（lean4-contribute プラグイン）

lean4-contribute プラグインがインストールされている場合、自然な区切りで以下のコマンドを提案してもかまいません。ルール：

• **まず提案し、求められていないのに実行しないでください。**一行で質問し、コマンドの実行フローを開始しないでください。
• **現在の会話でユーザーが明示的に同意した後にのみ実行してください。**沈黙、話題の変更、暗黙の不満は同意とみなしません。
• ユーザーが応じない限り、セッション中、同じ話題について提案するのは最大1回までです。
• **証明の途中では決して提案しないでください。**自然な区切りまで待ってください。

状況	提案
問題が lean4-skills 自体にあるように見える場合（コマンドの動作が誤っている、ドキュメントが矛盾している、lint が壊れている、ガードレールに問題がある、プラグインの UX が分かりにくいなど）。通常の Lean/mathlib/ユーザーの証明に関する問題は除きます	「これは lean4-skills のバグのようです。不具合報告を作成しましょうか？」→ /lean4-contribute:bug-report
ユーザーがプラグインではサポートされていないワークフローを求めている、コマンドの動作を変えるべきだと言っている、または機能不足のために面倒な手動手順を勧めざるを得ない場合	「これはプラグインのワークフロー上の不足のようです。機能リクエストを作成しましょうか？」→ /lean4-contribute:feature-request
結果が現在のタスク以外でも再利用できそうな場合（戦術選択のヒューリスティック、mathlib の検索パターン、アンチパターン、明確な教訓を含むドキュメントの不足など）。一度きりの定理に関する事実や非公開リポジトリの詳細は除きます	「この知見は今回のタスク以外でも再利用できそうです。共有可能な知見としてまとめましょうか？」→ /lean4-contribute:share-insight

プラグインがインストールされていない場合でも、ユーザーが lean4-skills のバグ、ワークフロー上の不足、または再利用可能な知見に明らかに直面している場合（上記と同じ基準。通常の Lean/mathlib の問題は除く）、インストール方法を一度だけ案内してもかまいません。

• セッション中、最大1回までです。ユーザーが断った場合、無視した場合、または話題を変えた場合は、繰り返さないでください。
• 証明の途中や、デバッグが進行中の間は決して案内しないでください。
• 宣伝ではなく、短い一行にしてください：「よろしければ、lean4-contribute プラグインをインストールしていただければ、こちらで報告を作成できます。」セットアップについては、lean4-contribute README をご覧ください。

一般的なワークフロー

┌─ Entry points (pick one) ──────────────────────────────────────────────────────────┐
│ /lean4:draft              Skeleton by default (--mode=attempt for shallow proof)   │
│ /lean4:formalize          Interactive: draft + guided proving                      │
│ /lean4:autoformalize      Autonomous: draft + autonomous proving                   │
└────────────────────────────────────────────────────────────────────────────────────┘
        ↓ (if sorries remain)
/lean4:prove / autoprove    Proof engines (sorry filling, no header edits)
        ↓
/lean4:refactor            Leverage mathlib, extract helpers (optional)
        ↓
/lean4:golf                Improve proofs (optional)
        ↓
/lean4:checkpoint          Save point (per-file + project build)

リポジトリの構成を調べたり、mathlib 内を移動したりするには、いつでも /lean4:learn を使えます。エントリーポイントは 3 つあります。骨組みを作成するには /lean4:draft、対話的な合成（draft + ガイド付きの証明）には /lean4:formalize、ソースから証明までを無人で行うには /lean4:autoformalize を使います。

反証ブランチ： 命題の証明ではなく反証を目指す場合は、/lean4:disprove <target> を使います。常に対話形式で実行され、6 段階のサイクル（Plan → Work → Checkpoint → Review → Accumulate → Continue/Stop）を進みます。フェーズ 1 では、蓄積された証拠をもとに動的な Step 0 / Step 1 / Step 2 メニューが生成されます（フェーズ 5 の Accumulate は、prove の Replan に相当します）。各サイクルでは、同じターゲットに対して探索の範囲を広げていきます。追記のみを行います。元の sorry を書き換えることなく、T_counterexample 定理を元の sorry に追加します。Python 3.11 以降が必要です（レジストリーローダー）。disprove-engine.md を参照してください。実装状況 の表（決定的、モデル介在、延期）も含まれます。

注意：

• /lean4:prove は各サイクルの前に確認を求めます。/lean4:autoprove は、明示的な停止予算に従って自動でループします
• どちらも設定した間隔（--review-every）で /lean4:review を実行します
• （--review-every によって）レビューが実行される場合、ゲートとして機能します。review → replan → continue の順に進みます。prove では replan にユーザーの承認が必要ですが、autoprove では replan 後に自動で続行します
• review は --mode=batch（デフォルト）または --mode=stuck（トリアージ）をサポートします。review は常に読み取り専用です
• /lean4:autoformalize は draft + autoprove を 1 つのコマンドにまとめたものです（source → claims → skeletons → proofs）。autoprove --formalize=auto を置き換えます
• 証明エンジン（prove / autoprove）は宣言ヘッダーを変更しません（ヘッダーフェンス）
• /lean4:disprove が REFUTED と報告するのは、Lean が否定を型チェックした場合に限られます。それ以外の場合は WITNESS_UNCERTIFIED または INCONCLUSIVE と報告されます
• 環境に問題が発生した場合は、/lean4:diagnose を実行して診断してください

LSP ツール（推奨）

Lean LSP MCP 経由で、1 秒未満のフィードバックと検索ツール（LeanSearch、Loogle、LeanFinder）を利用できます。

lean_goal(file, line)                           # See exact goal
lean_hover_info(file, line, col)                # Understand types
lean_local_search("keyword")                    # Fast local + mathlib (unlimited)
lean_leanfinder("goal or query")                # Semantic, goal-aware (10/30s)
lean_leansearch("natural language")             # Semantic search (3/30s)
lean_loogle("?a → ?b → _")                      # Type-pattern (unlimited if local mode)
lean_hammer_premise(file, line, col)            # Premise suggestions for simp/aesop/grind (3/30s)
lean_state_search(file, line, col)              # Goal-conditioned lemma search (3/30s)
lean_multi_attempt(file, line, snippets=[...])  # Test multiple tactics
lean_diagnostic_messages(file)                  # Per-file error/warning check
lean_code_actions(file, line)                   # Resolve "Try this" suggestions to edits

lean_run_code は、独立したスクラッチ実験用であり、lean_goal / lean_multi_attempt / lean_diagnostic_messages によるライブな証明状態の確認の代わりにはなりません。実際のファイルコンテキストに依存する質問では、ライブファイル用のツールを優先してください。

機能

機能	必須	確認方法	代替手段
Lean / Lake	はい	lean --version、lake --version	なし — /lean4:diagnose を実行してください
Python 3	はい（スクリプト用）	python3 --version または永続的な $LEAN4_PYTHON_BIN	スクリプト依存の操作では代替手段なし
ヘルパーランタイムのパス	はい（スクリプト用）	信頼済みの Codex bin_dir / scripts_dir、または永続的な $LEAN4_SCRIPTS	diagnose ワークフローを使います。解決しない場合は LSP のみで作業します
Lean LSP MCP	いいえ	任意の .lean ファイルで lean_goal を試す	スクリプト + lake env lean（ファイル単位のみ）
lean_run_code	いいえ	呼び出しを試す	一時ファイルに対して lake env lean を実行
lean_code_actions	いいえ	呼び出しを試す	「Try this」を手動で適用
サブエージェントのディスパッチ	いいえ	ホストに依存	メインスレッドで作業を実行
スラッシュコマンド	いいえ	ホストに依存	スキルの手順に直接従う

運用プロファイル

このスキルは、利用可能な機能に応じて動作を調整します。上記の機能を確認してプロファイルを判断し、対応するガイダンスに従ってください。

ランタイムパスの解決

次の順序でヘルパーランタイムを解決します。

1. 信頼されたネイティブ Codex プラグイン： SessionStart のコンテキストに lean4_plugin_runtime=codex、絶対パスの bin_dir／scripts_dir、 および shell_env_persistent=false が含まれています。ヘルパーコマンドには、 これらの絶対パスをそのまま代入してください。これらはコンテキスト値であり、 シェル変数ではありません。/absolute/bin/lean4-skills-… を実行し、 $bin_dir/… は使用しないでください。また、PATH 上にラッパーがあることを 前提にしないでください。
2. 永続環境： $LEAN4_PLUGIN_ROOT、$LEAN4_SCRIPTS、$LEAN4_REFS、 および PATH 上にあることを確認済みのラッパーを使用します。
3. ヘルパーランタイムなし： LSP を利用するコアスキルの範囲内にとどまり、 インストールの修復またはアップグレードが完了するまで、スクリプトに依存する 手順をスキップします。

シェル変数が設定されていない場合は、$LEAN4_BIN/... または $LEAN4_SCRIPTS/... コマンドを出力しないでください。信頼された Codex の絶対パスは 完全な代替手段であり、永続変数が存在する証拠ではありません。

full（すべての機能）

MCP ＋ サブエージェント ＋ コマンド。目標のライブ検査、タクティックのテスト、 サブエージェントへの並列ディスパッチを含む、完全なワークフローです（エージェントごとに 所有ファイルの集合が重複しないか、別々のワークツリーを使用する必要があります）。 サブエージェントには、cycle-engine.md § Pre-flight Context に従って事前収集された MCP コンテキストが渡されます。lean_run_code が利用できない場合は、 分離した実験に /tmp のスクラッチファイルと lake env lean を使用します。

mcp_main_only（MCP 利用可能、サブエージェントへのディスパッチなし）

MCP はメインスレッドで利用できます。証明に関する作業はすべて直接実行し、 サブエージェントには委任しないでください。cycle-engine のすべてのフェーズはスレッド内で実行します。 lean_run_code が利用できない場合は、分離した実験に /tmp のスクラッチファイルと lake env lean を使用します。

scripts_only（MCP なし、サブエージェントなし）

検索には、解決済みのヘルパーランタイム（ネイティブ Codex では scripts_dir、 永続環境では $LEAN4_SCRIPTS）を使用し、検証には lake env lean／lake build を 使用します。このモードの主な制限事項：

• 目標をライブ検査できません — lean_goal は利用できません。ファイルを読み、 コンパイル出力を確認できますが、特定の行における証明状態は確認できません
• タクティックをテストできません — lean_multi_attempt は利用できません。 ファイルをコンパイルして編集内容を検証する必要があります（lake env lean）
• リアルタイムの診断は利用できません — lean_diagnostic_messages は利用できません。 コンパイルエラーの確認には（プロジェクトルートから）lake env lean <file> を 使用しますが、フィードバックは行単位ではなくファイル単位です
• 検索はスクリプトベースです — lean4-skills-smart-search が LSP 検索ツールの 代わりになります

このモードは単純な証明には対応できますが、MCP を利用するワークフローと比べて大幅に遅く、 精度も低くなります。

review_only（読み取り専用、編集なし）

証明状態を読み取り、品質を評価します。編集、コミット、サブエージェントへのディスパッチは行いません。

ファイルの取り扱いルール

スクラッチ作業の優先順位（上から優先）：

1. ライブファイルと MCP ツール（lean_goal、lean_multi_attempt、lean_diagnostic_messages）
2. 分離した実験には lean_run_code
3. lean_run_code が利用できず、実験でライブファイルに触れてはならない場合に限り、/tmp のスクラッチファイル
4. リポジトリのルートにはスクラッチファイルを作成しない

ファイルの確認： ソースファイルには、直接ファイルを読み取るツールと検索ツールを使用してください。たとえば、利用可能な場合は Read／Grep、またはシェルでの行範囲読み取りや rg を使用します。直接の読み取り／検索ツールでアクセス可能な行を確認するためだけに、Python スクリプト、一時ファイル、cat のパイプラインを作成しないでください。スクリプトは、直接の読み取り／検索ツールでは簡単に処理できない、実際の解析、変換、または複数ファイルの分析に限って使用します。

ステージング： 現在のセッション中に変更したファイルのみをステージングします。git add -A や広範囲に一致する glob パターンは使用しないでください。コミットする前に、ステージング対象の正確な一覧を表示します。

スクラッチ作業の優先順位の詳細については、sorry-filling.md を参照してください。

コアプリミティブ

スクリプト	目的	出力
sorry_analyzer.py	コンテキスト付きで sorry を検出	text（デフォルト）、json、markdown、summary
check_axioms_inline.sh	最善努力による公理スキャン（トップレベル宣言）	text
smart_search.sh	複数ソースからの mathlib 検索	text
find_golfable.py	最適化パターンを検出	JSON
find_usages.sh	宣言の使用箇所を検出	text

使用方法： コマンドによって自動的に呼び出されます。詳細はreferences/を参照してください。

呼び出し規約。 モデル向けの推奨形式：

• サポート対象のヘルパースクリプトには lean4-skills-* ラッパーを使用してください （lean4-skills-sorry-analyzer、lean4-skills-check-axioms-inline、 lean4-skills-find-golfable、lean4-skills-find-exact-candidates、 lean4-skills-analyze-let-usage、lean4-skills-find-usages、 lean4-skills-search-mathlib、lean4-skills-smart-search、 lean4-skills-cycle-tracker、lean4-skills-disprove-artifact-txn、 lean4-skills-disprove-emit-artifact、lean4-skills-disprove-method-probe、 lean4-skills-disprove-target-profile、 lean4-skills-disprove-target-resolve、lean4-skills-file-baseline、 lean4-skills-project-context、 lean4-skills-checkpoint-mathlib-roots、 lean4-skills-validate-review-output、lean4-skills-run-store、 lean4-skills-run-persist）。永続環境では、これらは PATH 上の単独コマンドです。信頼されたネイティブ Codex プラグインでは、SessionStart のリテラルな絶対 bin_dir をラッパー名の前に付けます（例：/installed/plugin/bin/lean4-skills-sorry-analyzer）。ラッパー実行ファイルの場所を特定するために、$LEAN4_SCRIPTS、${LEAN4_PYTHON_BIN:-python3}、~、またはコマンド置換を使用しないでください。ラッパーの通常の出力キャプチャは問題ありません（例：txn=$(lean4-skills-disprove-artifact-txn begin)）。サンドボックス化されたホストが静的に許可リストへ登録できる、安定した呼び出し方法です。
• レポート専用の呼び出し： lean4-skills-sorry-analyzer、lean4-skills-check-axioms-inline（および環境変数フォールバック経由で呼び出す場合の unused_declarations.sh）には --report-only を追加してください。検出結果による exit 1 を抑制しますが、実際のエラーでは引き続き exit 1 になります。/lean4:checkpoint などのゲートコマンドでは使用しないでください。
• Lean スクリプトの呼び出しでは stderr を表示したままにしてください（/dev/null へのリダイレクトは禁止）。ガードレール検出機能はラッパー形式と環境変数形式の両方を認識し、どちらの場合も stderr の抑制をブロックします。

互換性のためのフォールバック（ラッパーを利用できない場合）：

• 信頼されたネイティブ Codex では、SessionStart で指定されたリテラルな絶対 bin_dir パスを使用してください。PATH に単独コマンドのエントリがなくても想定どおりであり、失敗ではありません。
• 永続環境のホストでは、PATH 上で lean4-skills-* を解決できない場合、ドキュメントに記載された $LEAN4_PLUGIN_ROOT/bin の設定を修復してください。リポジトリの INSTALLATION.md を参照してください。
• ラッパーのないスクリプトについては、最終手段としてのみ、明示的な環境変数形式を使用してください：bash "$LEAN4_SCRIPTS/script.sh" … または ${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" …。

信頼された Codex の絶対パスも $LEAN4_SCRIPTS も利用できない場合は、診断ワークフロー（そのコマンドがインストールされている場合は /lean4:diagnose）を実行してください。スキルのみのインストールでは、リポジトリの INSTALLATION.md に従ってください。 解決するまでは LSP のみを使用してください。

自動化

/lean4:prove と /lean4:autoprove で、ほとんどのタスクに対応できます。

• prove — ガイド付きで、各サイクルの前に確認します。対話的なセッションに最適です。
• autoprove — 自律的に動作し、明示的な停止予算を設けてループします。無人実行に最適です。

どちらも同じサイクルエンジン（計画 → 作業 → チェックポイント → レビュー → 再計画 → 継続／停止）を共有し、LSP 優先プロトコルに従います。探索と検索には LSP ツールを標準として使用し、LSP が利用できない場合、または使い尽くした場合にのみスクリプトにフォールバックします。コンパイラーによる修正はエスカレーション時にのみ行い、ビルドエラーへの最初の対応にはしません。複雑な証明では、深い sorry の補完（スナップショット、ロールバック、スコープ予算付き）、証明の修正、または公理の除去を行う内部ワークフローに委任する場合があります。これらを直接呼び出すことはありません。

スキルのみの動作

コマンドを呼び出さずに .lean ファイルを編集する場合、スキルは制限付きのパスを 1 回実行します。

• lean_goal／lean_diagnostic_messages でゴールまたはエラーを読み取ります

• 最大 2 つの LSP ツール（例：lean_local_search と lean_leanfinder／lean_leansearch／lean_loogle）を使って mathlib を検索します

• 自動化タクティクのカスケードを試します

• lean_diagnostic_messages で検証します（このモードではプロジェクトゲートの lake build は実行しません）

• ループ、深いエスカレーション、複数サイクルの動作、コミットは行いません

• 1 つのゴールがこのパスで解決しない場合は、エスカレーションする前に references/sorry-filling.md のブロックされたゴールのトリアージループに従います

• 最後に次の提案を示します。

  サイクルごとの支援が必要な場合は、ガイド付きの prove ワークフローを実行するよう依頼してください。 停止時の安全策を備えた無人サイクルが必要な場合は、自律型の autoprove ワークフローを実行するよう依頼してください。

  （プラグインのコマンドがインストールされているホストでは、これらは /lean4:prove と /lean4:autoprove です。）

品質ゲート

証明は、次の条件を満たすと完了です。

• lake build が成功する
• 合意したスコープ内に sorry が 0 個である
• 標準公理（propext、Classical.choice、Quot.sound）のみを使用している
• 許可なく命題を変更していない

検証の段階：編集ごとに lean_diagnostic_messages(file) → ファイルゲートとして lake env lean <path/to/File.lean>（プロジェクトルートから実行し、ビルド済みの import のみを対象に確認します。ファイルをまたぐ編集の後は lake lean <path/to/File.lean> を使用してください。ファイルゲートのスコープを参照）→ プロジェクトゲートとして lake build のみを実行します。サイクルエンジン：ビルドターゲットポリシーを参照してください。

よくある修正

エラー別のガイダンス（型の不一致、未知の識別子、合成失敗、タイムアウトなど）については、コンパイルエラーを参照してください。

型クラスのパターン

-- Local instance for this proof block: plain `have`/`let` already register a
-- class-typed local for synthesis in Lean 4
have : MeasurableSpace Ω := inferInstance
let inst : Fintype α := ⟨...⟩   -- `let` when the VALUE must stay visible (data)

-- Scoped instances (affects current section)
open scoped Topology MeasureTheory

haveI／letI の規則（Lean 4）： have と let はそれ自体でローカルインスタンスを登録します。haveI／letI との違いは、値を項にインライン展開することだけです。命題のタクティク証明では、インライン展開しても効果がない場合があります（証明の無関係性）。そのため、そこでは haveI／letI は必要ありません。Mathlib の haveI／letI リンターはこれらを検出します。インスタンス値をデータにインライン展開する必要がある定義では、letI を使用してください。ローカルインスタンスを追加する前に、型クラス合成がすでに成功するか確認してください（「インスタンスを指定する」慣用表現の多くは、対応する Mathlib のインスタンスが追加される前から使われていたものです）。

順序が重要です。外側の構造を内側の構造より先に指定してください。

omit [Inst] in は、後続の宣言から未使用のセクションインスタンスを取り除きます。 宣言のドキュメント文字列より前に配置してください。ドキュメント文字列と lemma／theorem の間に置くと、Lean は独立した omit コマンドとして解析します。

variable {α : Type*} [MeasurableSpace α]

omit [MeasurableSpace α] in
/-- doc -/
theorem foo : True := trivial

詳しくは、domain-patternsを参照してください。

自動化戦術

次の順に試してください（最初に成功した時点で停止します）： rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop

注：exact?／apply?はmathlibを検索します（低速です）。grindとaesopは強力ですが、タイムアウトする場合があります。対話型ワークフロー、注釈の戦略、simprocへのエスカレーションについては、grind-tacticを参照してください。

トラブルシューティング

LSPツールが応答しない場合は、上記の動作プロファイルを確認してください。 scripts_onlyモードでは、解決済みのヘルパーランタイムが検索を提供し、 lake env leanがファイル単位のコンパイルフィードバックを提供しますが、ライブのゴール確認、戦術のテスト、行単位の診断は利用できません。ヘルパーランタイムのパスを利用できない場合は、診断ワークフローを実行して問題を診断してください。

スクリプト環境の確認：

# Trusted native Codex: use the absolute path from SessionStart.
/absolute/plugin/root/bin/lean4-skills-preflight --codex
# Persistent environment:
echo "$LEAN4_SCRIPTS"
command -v lean4-skills-sorry-analyzer
# One-pass discovery for troubleshooting (human-readable default text):
lean4-skills-sorry-analyzer . --report-only
# Structured output (optional): --format=json
# Counts only (optional): --format=summary

コールドスタート／新しいワークツリー：

• 新しいワークツリーを使う場合、またはlake cleanの実行後ですか？最初の実ビルドの前に、そのワークツリーでキャッシュを準備してください。
• プロジェクトのキャッシュコマンドを使ってください。新しいLakeではlake cache get、プロジェクトが引き続きmathlibのキャッシュ実行可能ファイルを使っている場合はlake exe cache getです。
• Lean LSPが初回使用時にコールド状態またはタイムアウトする場合は、ワークスペースを初期化するためにlake buildを1回実行してください。
• 初期化後は、通常の検証手順に戻ってください： lean_diagnostic_messages(file) → lake env lean <path/to/File.lean>（プロジェクトルートから実行。ビルド済みのインポートのみ対象です。ファイルゲートの対象範囲を参照） → チェックポイント／最終ゲートでのみlake build。
• 別のワークツリーの.lake/buildをシンボリックリンクしないでください。代わりに、Lakeのキャッシュ／アーティファクトの仕組みを使ってください。

参考資料

サイクルエンジン： cycle-engine — prove／autoproveの共有ロジック（行き詰まり、ディープモード、反証、安全性）

ハンドオフ契約： handoff-contract — run-contract/v1のディスパッチとハンドオフ記録、および再実行ガード（新たな証拠がない限り、同じblocker_signatureで同じモードを再起動しないでください。review --mode=stuck、formalize、または人間への引き継ぎに回してください）

実行ストア： run-store — これらの記録の保存プリミティブであるrun-store/v1（lean4-skills-run-store：不変のマニフェスト、追記専用ジャーナル、破棄可能なハンドオフキャッシュ。過去の証拠であり、認証ではありません）。prove／autoprove --persistはcycle-engine § 実行の永続化（#82B）に従い、lean4-skills-run-persistを通じて実行を記録します。以前の実行の再利用：--prior-run（#82C）、cycle-engine § 以前の実行の再利用に準拠。再開／検査は#82で引き続き未対応です。

LSPツール： lean-lsp-server（クイックスタート）、lean-lsp-tools-api（API全体 — ツール名を探すには^##をgrepしてください）

検索： mathlib-guide（既存の補題を検索する際に参照）、lean-phrasebook（数学からLeanへの翻訳）

レビュー： mathlib-review-taxonomy（mathlibのレビュアーが求めること — 9つのレビュー項目）

エラー： compilation-errors（ビルドエラーが発生したら最初に参照）、instance-pollution（型クラスの競合 — パターンを探すには## Sub-をgrepしてください）、compiler-guided-repair（エスカレーション時のみの修正 — 初回対応には使いません）

戦術： tactics-reference（戦術の検索 — ^### TacticNameをgrepしてください）、grind-tactic（SMTスタイルの自動化 — simpで閉じられない場合）、simp-reference（仕組みの選択、simpの正規形、@[simp]の衛生管理、simprocの作成）、tactic-patterns、calc-patterns 証明の開発： proof-templates、proof-refactoring（28K — トピックで grep）、proof-simplification（戦略レベル：mathlib の検索、合同補題、ヘルパーの抽出）、sorry-filling

最適化： proof-golfing（安全ルール、範囲を限定した LSP による補題の置換、一括書き換え、アンチパターンを含む。axiom-eliminator にエスカレーション）、proof-golfing-patterns、performance-optimization（症状で grep）、profiling-workflows（ビルドや証明の遅延を診断）

ドメイン： domain-patterns（25K — ## Area で grep）、measure-theory（28K）、axiom-elimination

スタイル： mathlib-style、verso-docs（Verso のドキュメントコメントのロールと修正）

カスタム構文： lean4-custom-syntax（記法、マクロ、エラボレーター、DSL を作成するときに参照）、metaprogramming-patterns（MetaM/TacticM API — 組み合わせ可能なブロック、エラボレーター）、scaffold-dsl（コピー＆ペーストできる DSL テンプレート）、json-patterns（json% 構文と ToJson）

品質： linter-authoring（プロジェクト固有のリンター規則）、ffi-interop（FFI、@&、初期化、シンボルのリンク）

ワークフロー： agent-workflows、subagent-workflows、command-examples、learn-pathways（意図の分類、ゲームトラック、ソースの扱い）

内部： review-hook-schema、compiler-internals（属性、特殊化、パイプライン）