09:44
arXiv: DeepSeek@Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia
精选73°
推荐理由：形式化证明领域终于有了计算高效的实用方案——4B 模型就能超越 671B 巨无霸，做定理证明或形式化验证的团队可以直接用，省下大量算力成本。
精选
过去 24 小时，从 1007 条中筛出 58 条
6月12日
09:44
Pythagoras-Prover 是一个计算高效的 Lean 定理证明器系列，包含 4B 和 32B 参数的自回归模型，以及首个基于扩散的证明器（4B）。通过课程式监督微调和动态证明过滤，训练效率大幅提升。其 4B 模型在 MiniF2F-Test 上以 86.1% 的 pass@32 超越 DeepSeek-Prover-V2-671B（82.4%），参数减少约 167 倍；32B 模型达到 93.0%，创下开源新纪录。团队还提出了增强型 Lean 形式化方法（ALF），通过扰动已知问题生成变体，减少对表面形式的依赖，并发布了 MiniF2F-ALF 基准。
6月11日
15:28
AITOP6月11日 15:28
15:23
AITOP6月11日 15:23
15:07
AITOP6月11日 15:07
6月9日
11:52
11:52
arXiv cs.AI@Wesley Pegden
精选
推荐理由：Trellis 解决了自动形式化中可靠性与成本之间的平衡问题，做定理证明或形式化验证的开发者可以直接用这个工作流来生成 Lean 证明，值得关注其开源实现。
6月1日
00:09
AITOP6月1日 00:09
5月22日
11:11
11:11
arXiv cs.AI@George Tsoukalas, Anton Kovsharov, Sergey Shirobokov, Anja Surina, Moritz Firsching, Gergely Bérczi, Francisco J. R. Ruiz, Arun Suggala, Adam Zsolt Wagner, Eric Wieser, Lei Yu, Aja Huang, Miklós Z. Horváth, Andrew Ferrauiolo, Henryk Michalewski, Codrut Grosu, Thomas Hubert, Matej Balog, Pushmeet Kohli, Swarat Chaudhuri
精选72°
推荐理由：数学研究者终于有了能真正解决开放问题的 AI 工具——成本可控且覆盖多个数学分支，做组合数学或图论的人可以直接用这个智能体尝试自己的猜想。