形式定理证明

OProver：一个用于Lean 4的统一Agentic形式定理证明框架

OProver是一个用于Lean 4的统一Agentic形式定理证明框架，其核心创新是将迭代修订和反馈循环直接整合到证明器的训练过程中。该框架通过持续预训练和迭代后训练，并利用名为OProofs的大型语料库（包含177万条Lean语句和686万条编译器验证的证明）进行训练。据称，OProver-32B模型在MiniF2F、ProverBench和PutnamBench等基准测试中取得了领先的Pass@32成绩。