BBFM 猜想形式化获进展,AI 数学证明工具再下两城
ctjlewis · x · 2026-09-19
研究者宣布 BBFM 猜想形式化进展:已在 Lean 等形式化系统中完成猜想 6 的单峰性(unimodality)命题对全部 n ≥ 2 的证明,以及猜想 4 对 n ≥ 2^(10^8) 范围的证明。该工作建立在 Axiom Math 此前成果之上,补上了遗留的开放问题,展示 AI 辅助形式化数学的持续推进。
「研究」频道最新
- 基因组语言模型设计出自然界不存在的生物合成装配线 — KevinKaichuang · 2026-09-19
- 研究者质疑抗体模型用 SabDab 训练至 2025,测试集污染存疑 — anshulkundaje · 2026-09-19
- 淋巴瘤确诊后离开耶鲁,研究者转做抗体药物基础模型 — anshulkundaje · 2026-09-19
- WetRobo:让编码 Agent 在真实生物实验室里写程序操控机械臂 — sherryyangML · 2026-09-19
- NanoGPT Speedrun 新纪录 67.6 秒:屏蔽非规范 token 省 15 步训练 — kellerjordan0 · 2026-09-19
- Grigore Rosu：程序执行即证明生成，可无限产出训练数据 — LingmingZhang · 2026-09-19