The Erdős Frontier Atlas

这是一个可引用、机器可验证的地图，记录了围绕Erdős问题的计算前沿数据。它包括三层机器可读数据：hub索引所有约1217个Erdős问题（ID、状态、奖项等），deep tier包含51个经过审计的问题（带有验证器和当前记录），gap map是领域分类账，记录222个有界量及其置信度类别。数据集旨在通过计算映射有限计算能实现的内容，而非主张奖项可解决。This is a machine-readable map dataset focused on the computational frontier of Erdős problems. It comprises three tiers: the Hub indexes approximately 1,217 Erdős problems in total; the Deep Tier contains 51 reviewed Erdős problems; and the Gap Map documents 222 bounded quantities and their corresponding confidence categories. This dataset is designed for continuous updates via autonomous AI Agents, and is verifiable by anyone. It prioritizes results attainable through finite computation, such as exact small-value tables and witness records, rather than making claims for Erdős prizes.

原始信息汇总

数据集概述：The Erdős Frontier Atlas

核心定位

这是一个前沿制图学（frontier cartography）的原型工具，围绕Erdős问题构建了一个可引用、可机器验证的计算前沿地图，由自主代理全天候运作，任何人都可以核查。

数据集结构

数据集由三个可机器读取的核心层组成：

1. 中心枢纽（HUB）

• 文件：atlas/stubs.json
• 内容：索引了约1217个Erdős问题的元数据，包括ID、状态、奖金、OEIS链接和形式化链接，作为 erdosproblems.com 的计算附录。

2. 深度审计层（Deep Tier）

• 文件：atlas/problems.json
• 内容：51个经过深度审计的问题，每个问题都配有固定的精确验证器、可溯源的当前记录和重新计算的棋盘分类（board class）。

3. 差距地图（Gap Map）

• 文件：atlas/gap_map.json
• 内容：包含222个有界量的分类账，记录其 [L, U] 区间。每个条目通过 evidence[] 块计算置信等级（C0–C3），由验证器自动计算而非人为断言。

数据范围与限制

• 不涉及Erdős奖金：atlas中的任何Erdős奖金都无法通过有限计算申领，所有主要奖金均与渐近性陈述相关。
• 有限计算能做的事：精确小值表、见证记录、已验证至N的前沿、已认证的不存在性证明。
• 已知的无效计算区域：记录在 atlas/walls.md 文件中，明确标注哪些计算是已知的浪费。

数据集文件结构

层级	文件
领域文件	FRONTIER_CARTOGRAPHY.md（章程）、book/（活书）、RELEASING.md（数据发布）
地图文件	atlas/stubs.json（1217问题枢纽）、atlas/problems.json（51深度审计）、atlas/gap_map.json（222量分类账）、atlas/jc-crater/（雅可比猜想影响范围）、atlas/walls.md（禁止进入列表）、atlas/effectivization_shortlist.json（围栏目标）、atlas/lanes.md（求解器通道）
证据文件	certificates/（包含独立验证器和重播命令的证书目录）、observatory/（证书大小测量）、progress/（代理收据）
工具文件	tools/（验证器、生成器、编译器）、views/（生成的看板）、tests/（测试）

CHRONOS前沿看板（CHRONOS Frontier Board）

记录了CHRONOS代理在实际Erdős前沿上取得的进展，按验证等级分层：

等级	问题编号	贡献内容
🟢 已证明/已认证	#552	认证C₄-自由见证 ⇒ R(C₄,K₁,n) 公式
🟢 已证明/已认证	#241	证明B₃-子集表与序列关系
🟢 已证明/已认证	#13	认证精确表 f(1..45)
🟢 已证明/已认证	#979	a(6) > 10¹³ 于C1等级
🟡 已基础化/部分	#1107	验证 10¹⁰ 以下无例外
🟡 已基础化/部分	#142	完整的12,349个几何枚举
🟢 已证明/已认证	#1029 / #77	42个DRAT认证的结构性否定
🔴 已修正/已撤回	#552	之前的 =46 新值声明被撤回

形式化脊线锚点（Formal Spine Pins）

• 文件：atlas/lean_lane.json
• 内容：记录外部的Lean形式化工作，包括#593问题的完整有限分类和#625问题的部分检查点。

数据生成与维护

• 枢纽中的状态反映计算机分诊结果；upstream_status 在每次重建时从 erdosproblems.com 同步。
• 记录值和区间于2026-07-11根据原始来源验证。
• 数据集通过 tools/validate_atlas.py 进行验证，发布前需运行 python3 tools/validate_atlas.py。

引用

• 数据集标识符：EFA-DR1
• DOI：10.5281/zenodo.21443635
• CITATION.cff：位于仓库根目录

数据来源

• 问题索引来源于两个Apache-2.0许可的源：teorth/erdosproblems 和 google-deepmind/formal-conjectures。
• 不与 erdosproblems.com 竞争或镜像，仅为上游贡献已验证的记录。

搜集汇总

数据集介绍

构建方式

该数据集以Erdős问题为核心，围绕计算边界构建三层可机读结构。核心层（hub）索引约1217个Erdős问题，记录其编号、状态、奖金及OEIS与形式化链接，作为计算附录。深度层（deep tier）包含51个经审计的问题，每个均附有精确验证器、可溯源当前记录及重组后的黑板分类。间隙图谱（gap map）作为领域分类账，记录222个有界量及其上下界，每个条目附带证据块，由验证器自动计算置信等级（C0–C3），而非人工断言。数据来自自动代理挖掘与结构化验证，并通过`certificates/`目录提供独立于依赖的验证器与重放命令，确保可复现性。

特点

该数据集的卓越之处在于其诚实性与可验证性。所有记录均标明计算界限，明确无Erdős奖金可通过有限计算获取，避免虚假承诺。每个条目附带高置信度证据，且修正与撤回信息永久保留在分类账中，防止重复劳动。图谱涵盖已知无效计算边界（walls），明确标识计算资源的浪费点。此外，数据集通过机器同步与上游社区保持互补，而非镜像，确保信息最新。其模块化设计允许自动代理持续工作，提升边界记录，同时所有主张均可通过重放验证器独立检查。

使用方法

用户可通过一条命令（如`make hello-frontier`）快速验证证书，重放不存在性证明及其阴性对照，并打印带有计算置信等级的条目。数据集的各层文件（如`atlas/gap_map.json`）可通过指定工具（`tools/validate_gap_map.py`）进行校验。贡献者可通过提交问题或合并请求来质疑记录或上传新证据，代理则基于固定验证器在`automation/frontier-scout`分支上工作，待证据充分后升级至主干。此外，用户可在`views/`目录中查看生成的运行面板及操作附录，了解实时进展。

背景与挑战

背景概述

Erdős问题集是离散数学与组合学领域中一座丰碑般的知识宝库，自20世纪以来持续激发着数学家的探索热情。然而，随着问题规模的增长，有限计算所能触及的边界愈发模糊。《The Erdős Frontier Atlas》应运而生，由以CHRONOS自主代理为核心的团队于2026年创建，旨在为这些经典难题绘制一幅可机器验证、可引用的计算前沿地图。该项目对约1217个Erdős问题进行系统梳理，其中51个已通过深度审计并配备精确验证器，222个带界量被纳入缺口地图，以置信等级C0至C3加以标注。该数据集的核心研究问题在于：如何通过有限计算为无穷问题提供可验证的边界证据，而非直接求解。其独创的前沿制图学范式，不仅为数学计算领域提供了可复现的基准与透明的边界墙，更重塑了人机协作解决开放难题的生态，对形式化验证与自动化推理领域产生了深远影响。

当前挑战

该数据集面临的首要挑战在于所研究问题的本质困境：Erdős问题的核心奖项均与渐近性陈述绑定，任何有限计算都无法直接摘取这些桂冠，物理可验证的边界极限至多只能触及4/10的满分。其次，构建过程遭遇了数据的动态性与错误传播问题，上游问题状态随时间迁移，且曾发生AI生成条目（如A391599）渗入数据源的陷阱。更棘手的是，自主代理在闭环作业中可能重复解算已被社区关闭的问题，例如#552号问题曾因上游状态同步失效而显示已闭合的单元格为开放。此外，边界墙的标识需要精确判断，以警惕在READY/HEAVY这类模糊分界线上投入无效算力，而#165号问题即是此类判断失误的典型近例。

常用场景

经典使用场景

在计算数论与极值组合学的交叉领域，该数据集被广泛用于系统性地追踪埃尔德什问题的计算前沿。其核心应用在于为每个问题提供精确的有限计算界限（如小值表、见证记录、验证至某上限的前沿），并通过机器可验证的凭证结构实现断言的自动复现与审计。研究者利用该图谱快速定位已认证的进展，避免在已知计算壁垒上重复投入资源。

解决学术问题

该数据集有效解决了数论和组合学中大量未定界问题缺乏系统化、可验证计算证据的长期困境。通过为222个有界量提供支持度等级（C0–C3）和可重放验证流程，它弥合了理论陈述与可计算边界之间的鸿沟。其深远意义在于建立了一种可溯源、可修正的学术记录范式，使得计算型结果能够像定理证明一样被严格检验和持续更新。

衍生相关工作

基于该数据集及其验证优先方法论，已涌现出一系列衍生工作。典型代表包括针对R(5,5)问题的42项DRAT认证结构证伪库、对极吻界值的精确计算、以及自卷积不等式和素数定理常数的机器验证凭证集。这些工作均继承了同一凭证模板——结果优先的README、精确锁定的验证器、机器可检查的凭证和Zenodo DOI归档，构建起一个不断扩展的可验证计算证据生态系统。