# 策展 · X (Twitter) 🔥

> 📖 本站完整內容索引（documentation index）：[llms.txt](/llms.txt)

> 作者：Jichen Feng (@jcfeng27) · 平台：X (Twitter) · 日期：2026-04-13

> 原始來源：https://x.com/jcfeng27/status/2043157963863388220

## 中文摘要

MathCode v0.1.0 發布，強化數學形式化證明能力。

MathCode 是一個終端 AI 程式撰寫助手，專注於數學形式化引擎。本次 v0.1.0 更新引入了多項核心功能，旨在透過 Agent 協作與結構化證明，提升數學問題的解決效率。

**v0.1.0 重大更新**
本次更新大幅擴展了系統的證明與規劃能力，主要新增功能包括：
- Tree of Subgoals：支援將複雜數學問題拆解為子目標，並分配給多個 Agent 進行並行處理，顯著提升證明速度與效能，並支援多層級結構。
- TheoremLib：允許使用者儲存已證明的定理，並將其納入個人定理庫，供未來證明時調用，實現逐步構建大型定理證明。
- AxiomLib：使用者可透過對話建立個人化公理（包含數學、物理或敘述邏輯），MathCode 將協助建立邏輯世界並進行驗證。
- Guide of Plans：系統能從對話中學習，協助制定證明計畫，特別適用於需要人類引導的複雜數學問題。
- Blueprint：支援撰寫 Markdown 文件，將定理到引理的證明架構視覺化。
- Tools and Skills：引入工具與技能擴充機制，鼓勵社群貢獻。

**系統架構與核心能力**
MathCode 透過自動將自然語言數學問題轉換為 Lean 4 定理來進行形式化證明，並具備以下關鍵特性：
- Persistent Lean REPL：啟用後，經過約 90 秒的預熱（匯入 Mathlib），後續編譯檢查僅需約 0.4 秒，實現近乎即時的錯誤偵測與證明確認。
- Agent-Mode Proving：將證明過程轉化為互動式對話，Agent 可使用工具進行迭代證明。
- Obsidian Theorem Graph：支援生成 Obsidian vault，將定理依賴關係視覺化為知識圖譜。
- 多規劃器（Multi-Planner）：支援並行運行多個規劃器，以獲取多樣化的證明策略。

**擴充性與部署**
系統具備高度擴充性，支援透過資料夾結構新增功能，並簡化了部署流程：
- 擴充機制：
    - skills/：存放 .md 文件以增加領域知識與證明策略。
    - tools/：存放 Python 腳本以增加分析工具。
    - plugins/：存放 plugin 資料夾以擴充指令、Agent 或 MCP 伺服器。
- 部署與環境：透過 `setup.sh` 腳本自動下載對應的 binary asset，並處理 Lean 工具鏈與環境設定。系統支援 Anthropic 等相容後端，使用者可透過環境變數進行配置。

## 標籤

CLI, Agent, 新產品, 開源專案, MathCode