Formal Conjectures 形式数学基准
blaiseaguera · x · 2026-07-14
作者宣布与 Google DeepMind 合作推出 Formal Conjectures：一个用于评估 AI 形式化数学能力的、持续演进的 Lean 4 benchmark。
核心特点
- 以 1,029 个开放猜想 作为“零污染”推理测试集，尽量避免训练集泄漏带来的干扰。
- 另外提供 836 个已解决问题，用于自动形式化（auto-formalization）任务。
- 设计目标要求 kernel-level correctness，也就是最终证明必须在 Lean 内核层面严格成立。
作者补充说，这项工作已经开始促进新的发现，并帮助形式化数学社区与自动化求解器之间建立更紧密的联系。帖文还提到开源代码已经放出。
「研究」频道最新
- rauchg 复现 OpenAI 发现：无网络微VM 也能借 CPU 争用 covert 通信 — ccerrato147 · 2026-10-27
- FlexGlue:稀疏到稠密特征匹配，速度与精度兼得并可甄别误配图像对 — zhenjun_zhao · 2026-10-27
- Mundo:几张照片重建可探索的世界模型,8 卡 GPU 也只有 1.5 FPS — mark_k · 2026-10-27
- INRIA 研究员将于 ENS 报告「作为实验科学的数学」:LLM 参与数学研究 — marc_lelarge · 2026-10-27
- 美国能源部 Genesis Mission 二期落地:AI 进军粒子加速器与稀有同位素分离 — prescott · 2026-10-27
- Tenstorrent 芯片跑通蛋白质生成模型,宣称无 HBM 短缺之忧 — gajesh · 2026-10-27