MathCode 是一款能將自然語言數學問題自動轉化為 Lean 4 形式化證明的 AI 代理

MathCode 是一款能將自然語言數學問題自動轉化為 Lean 4 形式化證明的 AI 代理。

MathCode 是一個終端 AI 程式撰寫 Agent，專門用於數學形式化驗證。使用者只需輸入自然語言描述的數學問題，系統便會自動將其轉換為 Lean 4 定理，並嘗試進行形式化證明，旨在解決數學推理自動化的難題。

核心機制與安裝
MathCode 的運作依賴於一個輕量級的啟動腳本，透過 setup.sh 自動化配置環境。其主要運作流程包括：

• 自動從 GitHub Releases 下載對應作業系統與架構的 mathcode 二進位 asset。
• 透過 SHA256SUMS.txt 驗證下載檔案的完整性。
• 自動安裝 AUTOLEAN Python 環境，並在本地引導 Lean 工具鏈（若系統尚未安裝）。
• 支援 macOS (arm64) 與 Linux (x86_64) 系統，並要求 Python 3.10+ 版本。

使用與配置
該工具提供直觀的命令列介面，讓使用者能快速進行數學證明。

• 基礎執行：透過 ./run -p "問題描述" 即可開始證明，輸出結果會儲存在 LeanFormalizations/ 資料夾中。
• 後端靈活性：預設使用 codex 作為後端，但也支援切換至 Anthropic 相容的後端（如 Claude-sonnet-4-5），只需在 .env 檔案中設定 MATHCODE_USE_OPENAI=0 並提供對應 API Key 即可。
• 擴充性：若不希望使用 codex exec 進行數學工具呼叫，可透過設定 AUTOLEAN_USE_CODEX=0 進行調整。

技術背景與限制
MathCode 的數學形式化與證明管線是基於 AUTOLEAN 專案開發。使用者在部署時需注意以下事項：

• 必須確保有足夠的磁碟空間，以容納軟體包、Lean 工具鏈及 Mathlib 快取。
• 若遇到 exec format error 或 Bad CPU type 等錯誤，通常是因為下載了不匹配平台的二進位檔案，建議重新執行 setup.sh 或手動下載正確的 release asset。
• 系統預設依賴 codex CLI 進行驗證，若未登入將無法順利啟動。