# Pythagoras-Prover 发布 4B 参数定理证明器及扩散模型概念验证版

- 来源：Rohan Paul (@rohanpaul_ai)
- 发布时间：2026-06-16 06:58
- AIHOT 分数：58
- AIHOT 链接：https://aihot.virxact.com/items/cmqfu5j0y00ovslsp1g4qmr2q
- 原文链接：https://x.com/rohanpaul_ai/status/2066656699826786513

## AI 摘要

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.

### 引用推文

> Joshua Ong @ ICML：🚀🚀 Introducing Pythagoras-Prover 🚀🚀 🔹 The smallest theorem prover to date – Pythagoras-Prover-4B 🔹 The first proof-of-concept diffusion theorem proving mo...