數學工作流程
解決使用者提出的問題。不要將其變成一個廣泛的研究專案。
工作流程
- 重新陳述問題，並識別其數學領域。判斷使用者想要的是證明、計算、語料庫查詢還是形式驗證；僅澄清阻礙進行的歧義。
- 使用
math_search搜尋相關手稿和策略。從廣泛開始，然後按術語或假設進行縮小。使用math_manuscript只閱讀相關的摘要、大綱或 LaTeX 章節。如果缺少 TeX 原始碼或者您需要已發布的措辭，請對選定頁面使用math_pdf_text。 - 對於證明，在進行代數運算之前，先給出引理計劃。將從語料庫引用的結果與新的推導分開，並檢查每個引用結果的假設是否適用。
- 對於要求的形式驗證或 Lean 語句，使用
math_lean_search定位現有宣告，先對小片段使用math_lean_check，然後對聚焦目標使用math_lean_build。僅當存在匹配的挑戰配置時才使用math_comparator。預設情況下不要構建整個套件。 - 對於數值或符號工作，對允許列表中的 SymPy 操作使用
math_compute。否則，顯示計算過程並說明執行限制。數值證據不能證明精確斷言。 - 獨立檢查邊際情況、量詞、假設和中間步驟。確認每個 Lean 檢查是否實際通過以及檢查了什麼語句；一個通過的不相關片段並不能驗證所請求的定理。
語料庫和驗證護欄
math/CONTENTS.md映射了 373 個結果族中的 721 篇手稿。該檔案包含原始研究成果，而非經獨立認證的結果。- 目前有 175 篇論文具有 Lean 形式化；
math/lean/formalization.yaml是目錄。出現在目錄中並不證明論文中的每個斷言。 - 當結果看起來可疑時，請檢查
math/history.md；它記錄了修訂和撤回。不要盲目依賴撤回的結果。 - 絕不能僅僅因為一篇論文在語料庫中就聲稱其已被驗證。
- 除非相關的
math_lean_check、math_lean_build或math_comparator調用實際成功，否則絕不能聲稱 Lean 驗證。明確報告失敗、跳過的檢查、缺少的先決條件和剩餘的差距。 math/lean/是單一的 Lake 套件OAI，鎖定在leanprover/lean4:v4.34.1。優先使用聚焦目標，例如OAI.Analysis。- 使用
math_status檢查當前的可用性；不要將不可用的檢查視為成功。原生 Windows Lean 構建可能被鎖定依賴項集中 NTFS 無效的路徑阻止，而 Comparator/landrun 需要 Linux/WSL。報告此類障礙，而不是無聲地轉換斷言。 - 引用相對於
math/的來源路徑，例如lean/formalization.yaml，並在可用時附上手稿標識符和章節名稱。
工具使用模式
- 先廣泛查詢，然後縮小範圍；不要為局部問題進行全倉庫發現。
- 閱讀相關章節而非整份 PDF。根據元數據解析已發布的 PDF 路徑，而不是假設檔名；僅對選定頁面使用
math_pdf_text。 - 優先使用
math_grep在 TeX、Markdown 和 Lean 中查找確切名稱或符號；使用math_lean_search查詢宣告名稱。盡可能將搜索範圍限定到相關文件或目錄。 - 使用
math_compute進行符號檢查，但應說明操作並獨立驗證返回的表達式。 - 控制輸出大小：總結匹配結果，並僅引用必要的語句或證明步驟。
- 當
math/中的更改需要刷新索引時，使用math_reindex。
答案格式
- 定理 / 斷言： 精確的陳述、假設和範圍。
- 證明 / 推導： 引理計劃和經過驗證的步驟，或者請求的計算或查詢。
- 驗證狀態： 實際執行的檢查、結果及其覆蓋範圍的限制。
- 來源： 相關的語料庫路徑和章節；區分引用與新工作。
- 未解決的差距： 未解決的步驟或缺失的檢查，或明確表示未發現。