LEAP：通过智能体框架增强大语言模型的形式化数学能力

针对大语言模型在形式化语言（如 Lean）中生成可验证证明的困难，本文提出 LEAP 智能体框架。该系统利用基础模型的非正式推理与指令遵循能力，通过将复杂问题分解并持续与 Lean 编译器交互，桥接非正式蓝图与形式化证明构建。新提出的 Lean-IMO-Bench 基准测试显示，LEAP 将通用模型的单次求解率从不足 10% 提升至 70%，并在 2025 年普特南数学竞赛中解决了全部 12 道题目，展现了其在科研级复杂证明形式化中的实用价值。