Pythagoras-Prover 团队发布最小定理证明器 4B 版本及首个扩散模型概念验证版，均仅 4B 参数。在 MiniF2F 测试中，4B 模型以 86.1% Pass@32 超越 DeepSeek-Prover-V2-671B；32B 版本达 89.8% Pass@32 和 92.6% Pass@2024，创当前最佳成绩。核心在于数据效率：构造约 80 万 Lean 验证示例，按易到难训练，并采用 LoRA 微调避免全参数更新。模型上下文窗口为 8192 tokens。模型、数据及训练流水线将陆续开源。
Pythagoras-Prover just made Lean theorem proving look far less dependent on giant models, with a 4B prover beating DeepSeek-Prover-V2-671B at MiniF2F Pass@32.
Shows in formal reasoning, better data geometry can buy back an astonishing amount of scale.
A theorem prover is not just a language model writing clever math; it is a machine trying to produce text that survives a compiler with no patience for style, confidence, or almost-right reasoning.
The main trick is data efficiency: the team built about 800K Lean-verified examples, trained from easy to hard, then used LoRA so the model learned without updating every parameter.
🚀🚀 Introducing Pythagoras-Prover 🚀🚀 🔹 The smallest theorem prover to date – Pythagoras-Prover-4B 🔹 The first proof-of-concept diffusion theorem proving model – Pythagoras-Prover-Diffusion 4B With efficient LoRA training and an 8192-token context length, Pythagoras-Prover achieves strong MiniF2F results with far smaller models. 🏆 MiniF2F - Pythagoras-Prover-4B achieves 86.1% Pass@32, outperforming DeepSeek-Prover-V2-671B. - Pythagoras-Prover-32B achieves 89.8% Pass@32 and 92.6% Pass@2024, achieving the best MiniF2F result reported to date. 🌏Website: https://pythagoras-lm.github.io/ 📝 arXiv: https://arxiv.org/pdf/2606.12594 🤖 Pythagoras-Prover-4B: https://huggingface.co/Pythagoras-LM/Pythagoras-Prover-4B 🔐 Our models, data, and the training pipeline will be released (gradually) soon. A huge thank to my amazing collaborators: @zhengzhao97 @CMihaelaStoian Qiyuan Xu, @haonanlp @WendaLi8 Shay Cohen @e_giunchiglia在 X 查看被引用的帖子
来源：Rohan Paul · x.com