math-ai-org/mathcode

MathCode – AI 驅動的 Lean 編碼輔助工具

是什麼 – MathCode 是一個基於終端的 AI 編碼代理，協助您在 Lean 定理證明語言中撰寫、檢視與驗證形式化證明。它整合了 Lean 工具鏈、輕量級 Web UI，以及一組「技能」，讓模型能與 Lean 互動（搜尋宣告、檢查候選、驗證證明等）。

主要功能

• 目標導向的證明撰寫 – 提供自然語言目標（例如：「證明偶數的平方是偶數」），代理將迭代生成 Lean 程式碼，呼叫 Lean 工具，並優化證明。
• Lean 後端 – 代理可使用程序內 Lean REPL、固定子程序或外部 Kimina Lean 伺服器進行編譯與檢查。
• 持久化圖書館 – 您可將已證明的定理（/theorem-store）與對話式公理（/axiomatize）儲存在版本控制的保險庫中，供代理後續重用。
• Obsidian 圖譜匯出 – 產生定理依賴關係的視覺化知識圖譜，可在 Obsidian 中開啟。
• Web UI – 一個輕量級瀏覽器介面（./run webui），運行本地守護程序，並顯示與終端相同的互動式會話。
• 排程 – 使用 /loop 10m … 等斜線指令，可設定重複提示，用於提醒或定期檢查。

安裝與設定

1. 克隆倉儲並執行 bash setup.sh。該指令碼：
   • 如需，下載預先建置的執行時套件（mathcode-vX.Y.Z-<os>-<arch>.tar.gz）。
   • 使用 SHA-256 檢查碼驗證下載內容。
   • 安裝使用者本地啟動器（~/.local/bin/mathcode）。
   • 設定內建的 Lean 工具鏈（.local/elan）與快照式 Mathlib 儲存。
2. Linux 上必須安裝 bubblewrap（bwrap）與 socat；macOS 上該套件可開箱即用。
3. 如需使用預設的 OpenAI 支援模型，可選擇安裝 codex CLI。

典型工作流程

# 啟動互動式會話
mathcode -p "prove that the square of an even number is even"
# 或透過管道輸入
echo "hello" | mathcode -p

# 啟動 Web UI
./run webui

在會話中可使用斜線指令：

• /goal <budget> <objective> – 設定令牌預算並要求代理處理證明。
• /theorem-store …, /axiomatize … – 管理持久化定理／公理圖書館。
• /obsidian generate – 刷新 Obsidian 圖譜。
• /loop … – 設定重複提示。

設定選項（環境變數）可讓您調整系統，例如：

• MATHCODE_GOAL_MAX_TOKEN_BUDGET – 限制目標的令牌預算上限。
• MATHCODE_MAX_CHAINED_COMMAND_INPUTS – 限制代理可執行的巢狀工具呼叫次數。
• MATHCODE_LEAN_REPL – 強制使用程序內 REPL。
• MATHCODE_KIMINA_SERVER 及相關變數 – 指向外部 Kimina Lean 伺服器。

維護

• bash setup.sh --status 檢查二進位檔、檢查碼以及內建的 ripgrep 是否健康。
• bash setup.sh --clean 刪除安裝產物，但保留您的證明圖書館與 Lean 形式化內容。

適用對象 – 使用 Lean 並希望藉由 AI 驅動的助手加速定理證明、探索 Mathlib，並維護可重用形式化結果圖書館的研究人員、學生或開發者。

---

以上所有細節均直接取自倉儲的 README；未推斷任何額外功能。