AnnalsChallenge：Annals 数学年刊定理 Lean 形式化数据集
热点事件持续更新
AnnalsChallenge：Annals 数学年刊定理 Lean 形式化数据集
1 篇报道1 个报道来源8 小时前更新
先了解这件事
AI 综述
Kevin Buzzard、Thomas Browning 等发布 AnnalsChallenge 数据集：50 条用 Lean 4 手工编写、基于 Mathlib 的定理陈述，均取自 2020 年以来发表于《Annals of Mathematics》论文的主要结果。 每条形式化均经人工审查并由 AI 审计。数据集只包含定理陈述，不含形式化证明，适合作为自动定理证明的评测基准。
AI 根据报道生成 · 3 小时前更新
最新进展10月14日 12:00
AnnalsChallenge 发布《Annals of Mathematics》定理形式化数据集报道时间线
沿着报道，了解事件的不同侧面。
10月14日
- arXiv · cs.AIAnnalsChallenge 发布《Annals of Mathematics》定理形式化数据集
Thomas Browning 等发布 AnnalsChallenge 数据集，包含 50 个由作者手工编写的 Lean 4 形式化定理陈述，使用 Mathlib，覆盖 2020 年以来发表于《Annals of Mathematics》论文的主要结果。每条形式化均经人工审查并由 AI 审计，但数据集不包含形式化证明。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。