Lean 4 定理証明

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

コア原則

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

段階的に構築する。 Lean の型チェッカーはあなたのテストスイートです。sorry なしで、かつ標準公理のみでコンパイルされれば、証明は健全です。

スコープを尊重する。 ユーザーの嗜好に従ってください：1つの sorry、その推移的依存関係、ファイル内のすべての sorry、またはすべて。不明な場合は質問してください。

明示的な許可なしにステートメントを変更したり、公理を追加したりしないこと。 定理／補題のステートメント、型シグネチャ、およびドキュメント文字列は、ユーザーが変更を要求しない限り禁止です。インラインコメントは調整可能ですが、ドキュメント文字列は不可です（API の一部です）。カスタム公理には明示的な承認が必要です。証明が公理を必要とするように見える場合は、停止して議論してください。例外：合成ラッパー（/lean4:formalize、/lean4:autoformalize）内では、セッション生成宣言は外側ループのステートメント安全ルールに従って再草稿可能です（cycle-engine.md を参照）。

コマンド

コマンド	目的
/lean4:draft	非形式的なクレームから Lean 宣言スケルトンを草稿作成
/lean4:formalize	インタラクティブな形式化 — 草稿作成とガイド付き証明
/lean4:autoformalize	非形式的なソースからの自律型エンドツーエンド形式化
/lean4:prove	明示的なチェックポイント付きのサイクルバイサイクルガイド付き定理証明
/lean4:autoprove	ハードストップルール付きの自律型マルチサイクル定理証明
/lean4:checkpoint	安全なコミットチェックポイント付きで進捗を保存
/lean4:review	Lean 証明の読み取り専用コードレビュー
/lean4:refactor	mathlib を活用し、ヘルパーを抽出し、証明戦略を簡素化
/lean4:golf	Lean 証明の直接性、明確性、パフォーマンス、簡潔性を改善
/lean4:learn	インタラクティブな教学と mathlib 探索
/lean4:doctor	診断、クリーンアップ、移行支援

どのコマンド？

状況	コマンド
Lean スケルトンを草稿作成（デフォルトではスケルトン）	/lean4:draft
草稿作成 + インタラクティブに証明	/lean4:formalize
sorry を埋める（インタラクティブ）	/lean4:prove
sorry を埋める（無人）	/lean4:autoprove
検証済みセーブポイント	/lean4:checkpoint
品質チェック（読み取り専用）	/lean4:review
証明戦略を簡素化（mathlib 活用、ヘルパー）	/lean4:refactor
コンパイル済み証明の最適化	/lean4:golf
このプロジェクトは新規 / 探索中	/lean4:learn --mode=repo
トピックの mathlib をナビゲート	/lean4:learn --mode=mathlib
何かが機能していない	/lean4:doctor
エンドツーエンド形式化 + 証明（無人）	/lean4:autoformalize --source=... --claim-select=first --out=...

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

lean4-contribute プラグインがインストールされている場合、 自然な停止ポイントでこれらのコマンドを 提案 することができます。ルール：

• 提案を先に、自発的な呼び出しはしない。 ワンライナーの質問を提示してください。コマンドフローを開始しないでください。
• 現在の会話で明示的なユーザーオプトイン後のみ呼び出す。 沈黙、話題の変化、または暗黙の不満はコンセントとしてカウントされません。
• トピックあたり１セッションあたり最大１回 ユーザーが関与していない限り。
• 証明の最中は絶対に禁止。 自然な停止ポイントを待ってください。

状況	提案
問題が lean4-skills 自体に現れる（間違ったコマンド動作、矛盾したドキュメント、壊れたリント、不正なガードレール、混乱したプラグイン UX）— 通常の Lean/mathlib/ユーザー証明の問題ではない	「これは lean4-skills のバグのようです。バグレポートを草稿作成しますか？」 → /lean4-contribute:bug-report
ユーザーがプラグインが対応していないワークフローを望んでいる、コマンドが異なる動作をするべきだと言っている、またはプラグインの欠落機能のため厄介な手動ステップを推奨する必要がある	「これはプラグインワークフローギャップのようです。機能リクエストを草稿作成しますか？」 → /lean4-contribute:feature-request
結果は現在のタスク以上に再利用可能に見える：タクティク選択ヒューリスティック、mathlib 検索パターン、アンチパターン、明確な教訓を持つドキュメント化ギャップ — ワンオフ定理事実またはプライベート repo 詳細ではない	「それはこのタスク以上に再利用可能に見えます。共有可能な洞察を草稿作成しますか？」 → /lean4-contribute:share-insight

プラグインがインストールされておらず、 ユーザーが明らかに lean4-skills のバグ、ワークフロー gap、または再利用可能な洞察に遭遇した場合（上記と同じ基準 — 通常の Lean/mathlib 問題ではない）、インストールヒントを１回提供することができます：

• 1 セッションあたり最大 1 回。ユーザーが拒否、無視、または先に進んだ場合は繰り返さないでください。
• 証明の最中またはアクティブなデバッグループ中は絶対に禁止。
• ピッチではなく、短い１行：「必要に応じて lean4-contribute プラグインをインストールすれば、ここでレポートを草稿作成できます。」lean4-contribute README を参照してセットアップしてください。

典型的なワークフロー

┌─ エントリーポイント（1つ選択） ───────────────────────────────────────────┐
│ /lean4:draft              スケルトン（デフォルト、浅い証明は --mode=attempt） │
│ /lean4:formalize          インタラクティブ：草稿作成 + ガイド付き証明        │
│ /lean4:autoformalize      自律型：草稿作成 + 自律型証明                      │
└──────────────────────────────────────────────────────────────────────────┘
        ↓ （sorry が残る場合）
/lean4:prove / autoprove    証明エンジン（sorry 埋め、ヘッダ編集なし）
        ↓
/lean4:refactor            mathlib を活用、ヘルパーを抽出（オプション）
        ↓
/lean4:golf                証明を改善（オプション）
        ↓
/lean4:checkpoint          検証済みセーブポイント作成

リポジトリ構造を探索したり、mathlib をナビゲートしたりするために、任意の時点で /lean4:learn を使用してください。3つのエントリーポイント：スケルトンの場合は /lean4:draft、インタラクティブな合成（草稿作成 + ガイド付き証明）の場合は /lean4:formalize、無人ソースツープルーフの場合は /lean4:autoformalize。

注：

• /lean4:prove は各サイクルの前に質問します；/lean4:autoprove はハードストップ条件で自律型でループします
• どちらも設定された間隔（--review-every）で /lean4:review をトリガーします
• レビューが実行される場合（--review-every 経由）、それらはゲートとして機能します：レビュー → 再計画 → 続行。prove では再計画にはユーザー承認が必要です；autoprove では再計画は自動継続します
• Review は --mode=batch（デフォルト）または --mode=stuck（トリアージ）をサポートします；レビューは常に読み取り専用です
• /lean4:autoformalize は草稿作成+autoprove を単一コマンドにラップします（ソース → クレーム → スケルトン → 証明）；autoprove --formalize=auto に置き換わります
• 証明エンジン（prove/autoprove）は宣言ヘッダ（ヘッダフェンス）を変更しません
• 環境問題に遭遇した場合は、/lean4:doctor を実行して診断してください

LSP ツール（推奨）

Lean LSP MCP 経由のサブ秒フィードバックと検索ツール（LeanSearch、Loogle、LeanFinder）：

lean_goal(file, line)                           # 正確なゴールを表示
lean_hover_info(file, line, col)                # 型を理解
lean_local_search("keyword")                    # 高速ローカル + mathlib（無制限）
lean_leanfinder("goal or query")                # セマンティック、ゴール対応（10/30s）
lean_leansearch("natural language")             # セマンティック検索（3/30s）
lean_loogle("?a → ?b → _")                      # 型パターン（ローカルモードなら無制限）
lean_hammer_premise(file, line, col)            # simp/aesop/grind のプレミス提案（3/30s）
lean_state_search(file, line, col)              # ゴール条件付き補題検索（3/30s）
lean_multi_attempt(file, line, snippets=[...])  # 複数のタクティクスをテスト

コアプリミティブ

スクリプト	目的	出力
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/ を参照してください。

呼び出しコントラクト： スクリプト名を絶対に裸で実行しないでください。常に以下を使用してください：

• Python：${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/script.py" ...
• Shell：bash "$LEAN4_SCRIPTS/script.sh" ...
• レポート専用呼び出し：sorry_analyzer.py、check_axioms_inline.sh、unused_declarations.sh に --report-only を追加 — 検出時の exit 1 を抑制します；実エラーは依然として exit 1 となります。/lean4:checkpoint などのゲートコマンドでは使用しないでください。
• Lean スクリプトの stderr を可視に保ってください（/dev/null リダイレクトなし）。実エラーが隠されないようにするために。

$LEAN4_SCRIPTS が未設定またはないの場合は、/lean4:doctor を実行して、解決されるまで LSP のみを使用してください。

オートメーション

/lean4:prove と /lean4:autoprove はほとんどのタスクを処理します：

• prove — ガイド付き、各サイクルの前に質問します。インタラクティブセッションに最適。
• autoprove — 自律型、ハードストップルール付きでループします。無人実行に最適。

どちらも同じサイクルエンジン（計画 → 作業 → チェックポイント → レビュー → 再計画 → 続行/停止）を共有し、LSP-first プロトコルに従います：LSP ツールは発見と検索の規範です；LSP が使用不可能または枯渇した場合のみスクリプト フォールバック。コンパイラガイド修復はエスカレーション専用です — ビルドエラーへの最初の応答ではありません。複雑な証明の場合、深い sorry 埋め（スナップショット、ロールバック、スコープ予算付き）、証明修復、または公理排除のための内部ワークフローに委譲することがあります。これらを直接呼び出す必要はありません。

スキルのみの動作

コマンドを呼び出さずに .lean ファイルを編集する場合、スキルは 1つの有界パス を実行します：

• lean_goal/lean_diagnostic_messages 経由でゴールまたはエラーを読む
• 最大 2 つの LSP ツールで mathlib を検索（例えば lean_local_search + lean_leanfinder/lean_leansearch/lean_loogle）
• オートメーションタクティクスカスケードを試す
• lean_diagnostic_messages で検証（このモードではプロジェクトゲート lake build なし）
• ループなし、深いエスカレーションなし、マルチサイクル動作なし、コミットなし
• 提案で終了：

  ガイド付きサイクルバイサイクルヘルプの場合は /lean4:prove を使用します。 自律型サイクルとストップセーフガードの場合は /lean4:autoprove を使用します。

品質ゲート

証明は以下の場合に完了です：

• lake build が合格
• 合意されたスコープでゼロ sorry
• 標準公理のみ（propext、Classical.choice、Quot.sound）
• 許可なしのステートメント変更なし

検証ラダー：編集ごとに lean_diagnostic_messages(file) → ファイルゲート lake env lean <path/to/File.lean>（プロジェクトルートから実行） → lake build プロジェクトゲートのみ。cycle-engine: Build Target Policy を参照してください。

一般的な修正

エラーごとのガイダンスは compilation-errors を参照してください（型ミスマッチ、未知の識別子、インスタンス合成失敗、タイムアウト等）。

型クラスパターン

-- このプルーフブロックのローカルインスタンス
haveI : MeasurableSpace Ω := inferInstance
letI : Fintype α := ⟨...⟩

-- スコープインスタンス（現在のセクションに影響）
open scoped Topology MeasureTheory

順序が重要です：外側の構造を内側のものの前に提供してください。

オートメーションタクティクス

順序で試してください（最初の成功で停止）： rfl → simp → ring → linarith → nlinarith → omega → exact? → apply? → grind → aesop

注：exact?/apply? は mathlib を問い合わせます（遅い）。grind と aesop は強力ですがタイムアウトする可能性があります。grind-tactic を参照してください。インタラクティブワークフロー、注釈戦略、simproc エスカレーション用。

トラブルシューティング

LSP ツールが応答していない場合、スクリプトはすべての操作用のフォールバックを提供します。環境変数（LEAN4_SCRIPTS、LEAN4_REFS）がない場合は、/lean4:doctor を実行して診断してください。

スクリプト環境チェック：

echo "$LEAN4_SCRIPTS"
ls -l "$LEAN4_SCRIPTS/sorry_analyzer.py"
# トラブルシューティング用ワンパス発見（人間が読める形式のデフォルト text）：
${LEAN4_PYTHON_BIN:-python3} "$LEAN4_SCRIPTS/sorry_analyzer.py" . --report-only
# 構造化出力（オプション）：--format=json
# カウントのみ（オプション）：--format=summary

コールドスタート / 新規 worktree：

• 新規 worktree または lake clean 後？ 最初の実ビルド前にそのワークツリーでキャッシュをプライム化してください。
• プロジェクトのキャッシュコマンドを使用：新しい Lake では lake cache get、またはプロジェクトが依然として mathlib キャッシュ実行ファイルを使用している場合は lake exe cache get。
• Lean LSP がコールドまたは初回使用時にタイムアウトしている場合は、1 つの lake build を実行してワークスペースをブートストラップしてください。
• ブートストラップ後、通常の検証ラダーに戻ってください： lean_diagnostic_messages(file) → lake env lean <path/to/File.lean>（プロジェクトルートから） → lake build はチェックポイント/最終ゲートでのみ。
• 別のワークツリーの .lake/build をシンボリックリンクしないでください。代わりに Lake キャッシュ/成果物メカニズムを使用してください。

リファレンス

サイクルエンジン： cycle-engine — 共有 prove/autoprove ロジック（スタック、深いモード、偽造、安全性）

LSP ツール： lean-lsp-server（クイックスタート）、lean-lsp-tools-api（完全な API — ツール名は ^## grep）

検索： mathlib-guide（既存補題を検索する場合に読む）、lean-phrasebook（数学 → Lean 翻訳）

エラー： compilation-errors（ビルドエラーがある場合はまず読む）、instance-pollution（型クラス競合 — パターンは ## Sub- grep）、compiler-guided-repair（エスカレーション専用修復 — 最初パスではない）

タクティクス： tactics-reference（タクティク検索 — ^### TacticName grep）、grind-tactic（SMT スタイルオートメーション — simp でクローズできない場合）、simp-reference（simp 衛生 + カスタム simprocs）、tactic-patterns、calc-patterns

証明開発： proof-templates、proof-refactoring（28K — トピック grep）、proof-simplification（戦略レベル：mathlib 検索、congr 補題、ヘルパー抽出）、sorry-filling

最適化： proof-golfing（安全ルール、有界 LSP 補題置換、一括書き換え、アンチパターン包含；公理排除器へエスカレート）、proof-golfing-patterns、performance-optimization（症状別 grep）、profiling-workflows（遅いビルド/証明を診断）

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

スタイル： mathlib-style、mathlib-preferred-idioms（選択するべき抽象化）、verso-docs（Verso ドキュメントコメント役割とフィックスアップ）

入手可能性： mathlib-unavailable-theorems（依存関係として避けるべき定理 — 証明戦略を計画する前にチェック）

カスタム構文： lean4-custom-syntax（記号、マクロ、エラボレータ、DSL を構築する場合に読む）、metaprogramming-patterns（MetaM/TacticM API — 合成可能ブロック、エラボレータ）、scaffold-dsl（コピーペースト DSL テンプレート）、json-patterns（json% 構文 + ToJson）

品質： linter-authoring（プロジェクト固有のリンタルール）、ffi-patterns（Lake 経由 C/ObjC バインディング）

ワークフロー： agent-workflows、subagent-workflows、command-examples、learn-pathways（インテント分類法、ゲームトラック、ソース処理）

内部： review-hook-schema