Humanifa 登顶 LeanEval 榜单：249 题超 Axiom，饱和需形式化费马大定理
songhan_mit · x · 2026-10-21
LeanEval 团队宣布其数学形式化基准排行榜更新，Humanifa 工作流重新登顶。
- LeanEval 是目前唯一未饱和的数学形式化（Lean formalization）基准，据称要饱和它需要完成费马大定理的形式化。
- 榜单排名：Humanifa 以 249 题登顶，Axiom Prover（246）、Tau（200）、Aristotle/Harmonic（162）、Seed Prover/字节（156）分列其后。
- 团队称新的 Humanize 流程借鉴了 OpenAI、Anthropic 博客与 Axiom 技术报告的经验，“大定理”进展即将公布。
「研究」频道最新
- 仅 1 克！无线微型显微镜实现自由活动小鼠全皮层单细胞成像 — KordingLab · 2026-10-23
- Mike Frank 抛出超导可逆计算难题:能否用无偏置约瑟夫森结凑齐 BARCS 通用原语集 — MikePFrank · 2026-10-23
- Arc Institute 用基因组语言模型绘制原核非编码序列图谱 — tedgreenwald · 2026-10-23
- 同行评审的 AI 化：审稿人终于「进入附录」了 — abursuc · 2026-10-23
- Anthropic 用 Claude 为 100+ 开源库写下汇编级安全形式化证明 — AnthropicAI · 2026-10-23
- 研究提出 9 种策略为多 LLM 协作选模型，最优可超随机 36.1% — shangbinfeng · 2026-10-23