Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

Pythagoras-Prover 发布一组计算效率导向的 Lean theorem prover，包括 4B/32B 自回归模型和一个 4B diffusion-based prover 原型。训练上，它使用难度分层 Lean verified corpus、动态 proof-reasoning filtering 控制 8k 上下文，以及 Augmented Lean Formalisation 扩增形式陈述。最醒目的数字是 4B 在 MiniF2F-Test pass@32 达 86.1%，超过 DeepSeek-Prover-V2-671B 的 82.4%；32B 则达到 93.0%，并解出 PutnamBench 672 题中的 93 题。