Mathlib 定理探索のフローチャート

Mathlib 定理探索のフローチャート

定理を探す際は、「手軽で正確な方法」から順に試すのが鉄則です。

1. エディタ上での「逆引き」 (最速・正確)

証明を書きながら、Leanに直接探させる方法です。

• exact?: 「今のゴールを一撃で解ける定理はあるか？」
• apply?: 「一撃は無理でも、一歩進めるために適用できる定理はあるか？」
• rw?: 「現在の式を書き換えられる定理はあるか？」

2. 命名規則（Naming Convention）からの「推測」 (中速・正確)

Mathlibのルールに沿って名前を打ち、補完機能（IntelliSense）で絞り込みます。

• 基本形: 操作_対象_結論
• 例: $|x \cdot y|$ を展開したい → abs と mul が関係するはず → abs_mul と入力。
• 例: $a < b$ から $a+c < b+c$ を言いたい → add_lt_add_right ではないか？と予測。

3. 外部ツールでの「検索」 (低速・広範囲)

エディタで見つからない場合や、マニアックな定理を探す場合に使用します。

• Loogle (形・型で検索):

• | _ * _ | や Real |- _ < _ のように、記号や型を指定して検索。

• Moogle (意味で検索):

• triangle inequality や absolute value product のように、数学用語で検索。

4. AI（LLM）への「相談」 (柔軟・要検証)

「どう証明していいか方針自体がわからない」ときに有効です。

• 聞き方のコツ: 「この定理を Mathlib スタイルで書きたいです」と伝え、具体的な証明コードを見せる。
• 注意点: AIが提示した定理名が本当に存在するか、エディタ上で F12（定義ジャンプ）を押して確認する。

---

検索ツールの使い分けまとめ

手法	ツール/コマンド	使うタイミング
自動提案	exact? / apply?	とにかく今すぐ答え（次の行）が欲しい時
予測補完	VS Code (Ctrl+Space)	命名の規則性がなんとなく分かっている時
厳密検索	Loogle	使いたい記号や型の形が決まっている時
概念検索	Moogle	数学的な名前しか分からない時
方針相談	Gemini / ChatGPT	証明のロジック自体を相談したい時

---

このフローを繰り返すと、次第に「この定理ならこういう名前のはずだ」という感覚が養われ、検索の手間自体が減っていきます。

この整理について、さらに深掘りしたい部分はありますか？あるいは、今回の my_lemma のコードをもっと短くする「Mathlibらしい書き方」に興味がありますか？