MathCode

MathCode 把自然语言数学题转成 Lean 4 定理，再借助 Lean LSP、Loogle 和编译错误反馈循环修补证明，结果写入 `LeanFormalizations/`。它还提供子目标树、多规划器和 Obsidian 定理图谱，发布包覆盖 macOS arm64 与 Linux x86_64。相比只生成一段看似合理的推导，这套工作流把答案放进编译器可检查的形式证明边界内。