Lean 4 自動證明磨削。廣度優先掃描所有 sorry,按難度排序, 逐一嘗試證明,每解一個就 commit。搭配 lean-prover agent 做深度嘗試。 當用戶說「開始證明」、「grind」、「消除 sorry」、「prove all」時觸發。
From lean-provernpx claudepluginhub psychquant/psychquant-claude-plugins --plugin lean-proverThis skill uses the workspace's default tool permissions.
自動化消除 Lean 4 專案中的 sorry,直到 lake build 零錯誤或所有可解的 sorry 都已消除。
lean_project_path:Lean 4 專案根目錄(含 lakefile.toml),預設為當前目錄--max-attempts N:每個 sorry 最多嘗試次數(預設 8)--dry-run:只掃描和分類,不修改檔案# 找到 lakefile.toml 確認是 Lean 4 專案
# 確認 lake build 可以執行(即使有 sorry,不應有語法錯誤)
cd "$LEAN_PROJECT_PATH"
lake build 2>&1
如果有非 sorry 的編譯錯誤,先修那些。sorry 本身不算錯誤(Lean 會 warning)。
掃描所有 .lean 檔案,收集每個 sorry 的:
algebraic:目標是等式/不等式,可能用 ring, field_simp, nlinarith, linarith, norm_num 解api-bridge:需要找到正確的 Mathlib API(如 UI 定義橋接)structural:需要構造性證明(歸納、case split)deep:需要複雜的數學推理(測度論、拓撲)placeholder:結論是 True 或 trivial,需要重寫定理陳述# 掃描 sorry
grep -rn "sorry" --include="*.lean" "$LEAN_PROJECT_PATH" | grep -v "^.*:.*--.*sorry"
# 掃描 axiom(非 Mathlib 的)
grep -rn "^axiom " --include="*.lean" "$LEAN_PROJECT_PATH"
# 掃描 trivial placeholder
grep -rn ": True :=" --include="*.lean" "$LEAN_PROJECT_PATH"
按以下優先級排序(廣度優先):
| 優先級 | 類型 | 預期策略 |
|---|---|---|
| P0 | placeholder(: True) | 重寫定理陳述為真正的命題 |
| P1 | algebraic | ring, field_simp, nlinarith, norm_num, positivity, omega |
| P2 | structural | induction, cases, simp, exact, apply |
| P3 | api-bridge | 搜尋 Mathlib,找到對應的 lemma/theorem |
| P4 | deep | 需要 lean-prover agent 深度嘗試 |
輸出分類結果到 PROGRESS.md。
對每個 sorry(按優先級順序):
for sorry in sorted_sorries:
attempt = 0
while attempt < MAX_ATTEMPTS:
attempt += 1
1. 讀取 sorry 所在的完整定理和上下文
2. 根據類型選擇策略:
- algebraic → 嘗試 tactic 組合
- api-bridge → 用 Grep 搜尋 Mathlib 或 `exact?`, `apply?`
- structural → 分析目標結構,嘗試 induction/cases
- deep → 啟動 lean-prover agent(subagent)
- placeholder → 重寫陳述,然後按新類型處理
3. Edit .lean 檔案,替換 sorry
4. lake build(hook 會自動觸發,但這裡也要手動確認)
5. 如果成功:
- git commit -m "prove: {theorem_name} — eliminate sorry"
- 更新 PROGRESS.md
- break
6. 如果失敗:
- 讀取 lake build 錯誤訊息
- 分析錯誤類型(type mismatch, unknown identifier, tactic failed)
- 調整策略重試
if all attempts failed:
記錄到 PROGRESS.md:
- 定理名稱
- 嘗試過的策略
- 最後的錯誤訊息
- 建議的人工介入方向
還原 sorry(不要留 broken 的證明)
嘗試順序:
norm_numringfield_simp; ringnlinarith / linarithpositivityomega(自然數/整數)field_simp; nlinarithsimp only [...]; ring∀:intro∃:exact ⟨witness, proof⟩ 或 use witnessA ∧ B:constructorA ∨ B:left 或 rightA ∨ B:cases hinduction 或 casessimp [relevant_lemmas]grep -rn "theorem.*{keyword}" ~/.elan/toolchains/leanprover-lean4-v4.*/lib/lean4/library/
# 或在 Mathlib source 中搜尋
exact?(在本地 Lean LSP 中)exact Mathlib.Theorem.nameapply + 填補 arguments啟動 lean-prover agent(見 agents/lean-prover.md),給它:
完成後輸出:
## Grind Report
- 初始 sorry 數:N
- 已消除:M
- 仍然卡住:K(列表 + 原因)
- axiom 數(預期保留):A
- placeholder 數(需重寫):P
- lake build 狀態:✓ / ✗
### 卡住的 sorry
| 定理 | 檔案:行 | 類型 | 嘗試次數 | 最後錯誤 | 建議 |
|------|---------|------|----------|----------|------|
| ... | ... | ... | ... | ... | ... |
在 Lean 專案根目錄維護 PROGRESS.md:
# Proof Progress
Last grind: {date}
Status: {N}/{Total} sorries eliminated
## Completed
- [x] `rasch_deficiency_neg` — `nlinarith` (2025-04-02)
- [x] `thm3_deficiency_formula` — `field_simp; linarith` (2025-04-02)
## In Progress
- [ ] `thm1_second_order_separation` — needs MLE variance expansion (P4)
## Blocked
- [ ] `hoadley_thm1_consistency` — depends on A.3 + A.4 (P4)
## Intentional Axioms (not sorry)
- `thmA1_sufficient_ui` — Neveu (1965), standard measure theory
- `loeve_markov_wlln` — Loève (1960), p. 275
.lean 檔後自動 lake build/ralph-loop:ralph-loop 包裝本 skill 做持續運行axiom——它們是文章引用的外部結果True 的定理(placeholder)需要先重寫陳述再證明prove: {theorem_name} — eliminate sorrylake build 有非 sorry 的錯誤,優先修那些