MathCode：用自然语言自动证明数学定理

MathCode, Mathematical Coding Agent

MathCode 是一款终端 AI 编程助手，内置数学形式化引擎。用户只需输入自然语言描述的数学问题，它就能自动将其转化为 Lean 4 定理并尝试形式化证明。该系统拥有持久的 Lean REPL，编译检查时间从 30 秒缩短至 0.4 秒。它支持自动命名和存储已证明的定理，构建可复用的定理库和公理库，并通过 Lean LSP 集成搜索 Mathlib 引理。此外，MathCode 还能生成 Obsidian 知识图谱，可视化定理间的依赖关系，支持多规划器并行运行和子目标树分解，让复杂的数学证明过程变得高效且可交互。