Formal Conjectures：Lean 4 形式化数学基准发布
热点事件持续更新
Formal Conjectures：Lean 4 形式化数学基准发布
1 篇报道1 个报道来源3 小时前更新
先了解这件事
AI 综述
Google DeepMind 发布开源基准数据集 Formal Conjectures，将 7559 条数学问题陈述用 Lean 4 形式化，论文已被 NeurIPS 2026 Datasets and Benchmarks Track 收录。 数据集包含三类内容：1642 条无已知解的开放研究猜想，可用于数学证明发现；2923 道已解决问题，可用于证明自动形式化；另有 2994 条辅助命题。该基准定位为演进型数据集，内容会持续更新。
AI 根据报道生成 · 2 小时前更新
最新进展11月14日 13:00
Formal Conjectures：面向数学验证式发现的开源演进型基准报道时间线
沿着报道，了解事件的不同侧面。
11月14日
- arXiv cs.AIFormal Conjectures：面向数学验证式发现的开源演进型基准
Formal Conjectures 是一个用 Lean 4 形式化的数学基准，目前包含 7559 条数学问题陈述，其中 1642 条无已知解的开放研究猜想、2923 道已解决问题和 2994 条辅助命题，已收录于 NeurIPS 2026 Datasets and Benchmarks Track。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。