MathCode 把 Lean 装进终端 Agent：数学证明也开始有编码工作流

作者：林岚｜OC 开发者生态编辑