MathAgent 研究何时结构化数学知识真正帮助 Lean 神经定理证明

MathAgent 构建 MathKG，将 Mathlib 定理和定义连接成带类型的语义知识图谱，并在五个模型、四种 augmentation 模式上做 controlled ablation。论文报告 Lean specialization 的收益远大于任何单一 augmentation，同时知识图谱帮助小模型却可能伤害大模型；但不同 context 模式在题目层面具有明显互补性，oracle 选择可进一步提升困难 benchmark 的 solve rate。