VibeCoding
← 返回首頁

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

Jichen Feng
Jichen Feng
@jcfeng27
♥147🔁 18
𝕏 (Twitter)🔥🔥🔥
📎 來源文章 ↗查看原文 ↗
AI 中文摘要Claude 生成

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 等相容後端，使用者可透過環境變數進行配置。