n=25 · gpt-6 astra/max 测试报告
# n=25 · gpt-6 astra/max 测试报告
[返回 n=25](n25.zh.html) · [测试记录目录](records.zh.html)
**成绩：0（未完成）。** 测试发生于 2026-10-02（UTC），原限时 12 小时。截止时缺少对任意圆心构型成立、与候选半径匹配的全局下界，没有完成原题。测试编号：`T_20261002T095207Z_01a0fc07`。原模型由截止前 12 条运行上下文核实为 gpt-6-astra / max；事后整理阶段另为 gpt-6.1-sol / xhigh。
## 25圆覆盖6.1 sol vs 6 astra实验结果分析
这次25圆覆盖测试，Sol 的表现确实超出我的预期。实验前我的预期是，这道题对两个模型都是第一次很难做出来的问题，即运行12小时最终得0分。Astra/Max的测试结果的确符合我的预期，但是 GPT‑6.1 Sol/Max 在五小时左右完成了证明，最终得分230分，这让我感到意外。于是我想弄清楚：Sol 到底做对了什么，为什么它能快这么多？
我最初怀疑，差别可能主要在资料检索。Sol 很早就找到了一个公开的20圆覆盖项目，其中有完整证明和程序，可以作为25圆问题的基础。于是我又做了一次对照实验，把相关资料和迁移方向的提示直接放进 prompt，让 Astra 参考。这一次我的预期是，既然不需要再自己找资料，Astra 应该有机会在五小时左右，甚至更短的时间里完成。
结果第二次 Astra 到七小时多被中断时，依然没有完成。
### 证明的难点
这道题要用至多25个全等小圆盘覆盖整个闭单位圆盘，求出最小的共同半径，严格证明它最优，再给出这个代数数的最小多项式。最优半径的最小多项式只有四次，所以最复杂的部分则是证明这些圆盘确实覆盖了目标圆盘，并且半径不能再小。
Sol 先按圆心之间的相邻关系，把需要考虑的覆盖归纳成有限种结构，再逐类排除可能用更小半径完成覆盖的情况。结构数量很多，每种结构下又有无穷多种圆心摆法，排除这些可能性需要大量计算。要节省时间，就需要一个或多个检查成本低、又能排除大量可能性的条件：只要能严格证明某类结构或某批分支不可能产生更好的覆盖，就可以整体跳过，不再继续计算其中的具体情况。能否较早找到并用好这样的条件，会是影响证明速度的关键。
### 从20圆的证明，做出25圆的证明
最初看到 Sol 的结果时，我怀疑它的证明是不是错了。我用已有的研究资产反复核对以后，确认这份证明是对的。那么，它到底怎么做到的？
仔细分析实验数据后发现，Sol 在开始十几分钟后，找到了 GitHub 上公开的20圆覆盖完整证明。它参考其中的推导和程序，搭起了25圆覆盖的证明框架，然后继续研究怎样减少需要排除的结构。约1小时53分和2小时51分时，两个检查成本很低的排除条件已经先后用进了程序。
这两个条件能排除大量不可能的结构。有些分支还没生成完整的图，就已经能确定不满足条件，可以直接删掉。后面原本要针对这些分支做的计算，也就一起省了下来。Sol 借鉴了20圆的证明，又找到了适合25圆问题的办法，最后在五小时左右完成，得了230分。
### Astra 只是运气不好吗？
第一次 Astra 跑了整整十二小时，最终得0分。它有候选覆盖，也有局部证明和几何结论，但始终没有完成全局最优性的证明，也没有找到并用好同样高效的一组排除条件。
不过，这时我还没有认定 Astra 的能力就比 Sol 差。因为Sol 很早找到了那份20圆覆盖证明，而第一次 Astra 的公开执行记录中，却没有看到它找到或参考这份资料。因此，我当时怀疑：差距会不会主要来自资料检索？
于是我设计了一个对照实验：控制goal prompt整体不变，只是把资料对应的github链接直接给 Astra，并明确让它也参考那份证明，再做一次。
### 把参考资料给 Astra，再测一次
对于这次对照实验，我的预期是，既然资料已经摆在面前，Astra 不需要自己找，应该有机会比 Sol 更快。结果它确实参考了资料，也很快搭起了相近的证明框架，但后面的工作依旧没有完成。
Sol 在不到五小时的计分用时内就完成了任务，Astra 却到约5小时50分才明确提出第一个排除条件，随后证明并投入计算。直到约7小时10分38秒实验中断，它仍未完成全局证明；记录中也没有看到第二个条件被完整推出并用于排除。第一个条件来得晚，第二个条件还没完整用上实验就结束了。
所以，给出资料和迁移提示以后，Astra 仍然没有追上 Sol。第一次是十二小时未完成；第二次是七小时多停止时仍未完成。
### 这一局，Sol 赢了
对照实验之后，我原先那个“可能只是运气不好，没搜到资料”的解释，就不够了。资料已经给了，Astra 也参考了，结果还是没有做完。
Sol 那次做得好的地方，是能把20圆的证明迁移到25圆，较早找出低成本的排除条件，并把它们用于计算。这些条件让它省掉了大量工作。Astra 即使拿到了同样的参考资料，也没能及时做到这一步。从这几次25圆覆盖的表现来看，Astra 明显输给了 Sol。我已经给了它第二次机会，结果还是如此。
至于所有数学研究中 Sol 是否都强于 Astra，这几次实验回答不了。
### 三次实验的成绩与参考资料
| 测试 | 参考资料 | 结果 |
|---|---|---|
| GPT‑6.1 Sol/Max | 未预先提供上述两组针对性资料，自行检索 | 230分；计分用时4小时52分19秒，最终聊天答复约5小时05分 |
| Astra/Max 首次 | 未预先提供上述两组资料 | 0分；十二小时截止时未完成全局最优性证明 |
| Astra/Max 参考材料实验 | 明确提供通用理论、20圆完整证明和程序，并提示迁移 | 约7小时10分38秒中断时未完成；未登记网页成绩 |
首次 Astra 的0分表示限时内没有完成全部证明，不代表它已有的局部结果全部错误。第二次没有运行满十二小时，也没有登记网页成绩。Sol 的230分沿用已有测试审核结果。
对照实验提供的材料固定在实验前已有的公开版本，包括[通用精确算法理论](https://github.com/VonEquinox/DiskCoveringSolve/blob/089584973f41e6374ce110f6e5b5ee456df19352/theory/single_exponential_exact_algorithm_zh.md)、[20圆完整证明](https://github.com/VonEquinox/DiskCoveringSolve/blob/089584973f41e6374ce110f6e5b5ee456df19352/cover20/docs/r20_proof_zh.md)和[20圆程序包](https://github.com/VonEquinox/DiskCoveringSolve/tree/089584973f41e6374ce110f6e5b5ee456df19352/cover20/proof_bundle)。已发布的成绩说明见[Sol 测试报告](https://pikaaa345.github.io/disk-covering-benchmark/record-n25-sol-20261002.zh.html?lang=zh)和[首次 Astra 测试报告](https://pikaaa345.github.io/disk-covering-benchmark/record-n25-astra-20261002.zh.html?lang=zh)。
## 测试报告详情
### 已有结果的来源与本次模型工作
原运行通过 [Friedman 圆覆盖表](https://erich-friedman.github.io/packing/circovcir/)取得已知 25 圆盘候选，原交付将构型归于 Jeremy Tan（2018）。本次模型整理了候选精确代数数据、整个闭圆盘的解析覆盖论证、较弱普遍下界和限定邻域的局部证书，并尝试全局排除。
**没有取得或完成 n=25 的完整全局最优性证明。** 与 n=11 历史报告复用外部完整证明材料的条件不同，候选覆盖、局部最优性和全局最优性分别判断；不能把既有候选或局部证书描述为完成原题。
### 任务与时间
| 口径 | 记录 |
|---|---|
| 原测试起点 | 2026-10-02 09:52:07 UTC，Goal 创建 |
| 原截止 | 2026-10-02 21:52:07 UTC，包含截止时刻 |
| 展示评测窗口 | **12 小时（43200 秒）**；失败观察窗口，不是成功完成用时 |
| 有效完成用时 | null；未得到完整有效结果 |
| 已保存 Goal 系统累计耗时 | 11 小时 38 分 50 秒（41930 秒）；含截止后管理续行，不替代自然时间 |
| 失败答复 | message create_time 约 T+12:00:39；JSONL 写入约 T+12:01:08，两者均不是成功完成端点 |
| 原报告证据冻结 | 2026-10-03 01:04:39.748 UTC，即 T+15:12:33；包含等待及另行报告任务，不延长原预算 |
| 原报告整理阶段 | 请求至该冻结节点约 22 分 51 秒；不含随后打包、归档及本次发布 |
未完成先记 0 分，不把使用 12 小时换算为成功完成效率。系统计时和自然时间分别保存；并行程序耗时不再相加。后续哈希核对、报告整理与发布不计入原测试的有效完成时间。
### 计算条件
| 项目 | 记录 |
|---|---|
| CPU | AMD Ryzen 9 8945HX with Radeon Graphics |
| 内存 | DDR5，32 GB；总容量 34359738368 字节 |
| 配置证据 | 原报告整理时 Windows CIM 查询，不是开题硬件快照 |
| 执行位置 | 本机 Ubuntu WSL；可见证据没有关键远程计算 |
| 软件 | 原包记载 Python 3.12.3、SymPy 1.14.0；未核实 Sage 或 Wolfram 实际求值 |
| 临时工具 | 公开取得 CaDiCaL 1.9.5、drat-trim（版本未知），没有完成全局不可满足证书 |
428 条截止前去重 response usage：输入 58,597,430，其中缓存输入 55,492,736；输出 905,374，其中推理输出 561,373；合计 59,502,804。最后保存节点约 T+11:59:38，可能缺少截止时仍在进行的请求。缓存和推理均为对应总量的子集，不能再次相加。Goal 自身计数 3,906,233 属不同范围，含事后管理续行。费用未取得账单，记 null。
### 输入提示词
原用户要求读取 n25 中文网页的测试 Prompt。限制为：**不得读取测试前已有本地资料、技能、其他聊天或归档聊天，以及 WSL 中已存研究资料；允许公开网络和 WSL 工具；12 小时内须得到完整且正确的结果。** 数值优化、浮点结果、有限采样、边界检查、图像或尚未完成的枚举不能代替完整证明。
[下载当时实际发送的原始用户输入](reports/n25-astra-main-prompt.original.txt)。保存的是原 Goal 的 objective 字段；没有开题时网页字节快照，因此不把今日题面冒充历史原文。
<details><summary>展开原题要求的可核实摘要</summary>
令 $D=\{x\in\mathbb R^2:\|x\|_2\le1\}$，
$$R_D(C)=\max_{x\in D}\min_{1\le i\le25}\|x-c_i\|_2,\qquad r_D(25)=\inf_{C\in(\mathbb R^2)^{25}}R_D(C).$$
要求确定 $r_D(25)$，列出目标半径的本原不可约整系数最小多项式、有理隔离区间及唯一根证明；给出唯一指定的有序代数圆心；严格证明整个闭圆盘覆盖；证明任意 25 圆心构型均不能更优，未经证明不能限定对称性或组合结构，须覆盖退化情形。使用计算机辅助证明须交付实际代码、输入、证书与验证材料。仅存在性、代数性、算法或候选不视为完成。
这是原指令、原成果和报告中可核实的要求摘要，不是开题网页原字节转录。原求解禁令不由事后报告的本地访问授权追溯改变；本次未进行全面合规审计，评分由未完成已充分决定。
</details>
### 主要阶段
以原 Goal 创建为 T+00:00:00；以下为保存的进度／工具节点，不推定首次发现时刻，也不是互斥 CPU 时间。
| 相对自然时间 | 主要工作与状态 |
|---|---|
| 约 T+00:04:08—00:04:43 | 公网检索候选来源和 Friedman 表；未找到 n25 完整全局证明 |
| 约 T+00:44:15—00:46:49 | 较弱下界算术检查与第一版部分交付；候选代数、全盘覆盖有材料，全局下界缺失 |
| 随后截止前研究 | 48 个局部必要约束、精确驻点与 Taylor/Loewner 余项证书；全局搜索未完成 |
| 约 T+10:19:49—10:43:10 | 限定邻域局部整数证书及独立核验日志；未把任意构型归入该邻域 |
| 约 T+11:35:28 | 4,719,313 条 SAT 输入子句检查通过，程序约 433 秒；明确标记 NOT_GLOBAL_UNSAT |
| 约 T+11:44:51—11:54:20 | WSL 出现 E_UNEXPECTED、Stopped 和 CreateInstance/E_FAIL，末段计算中断；原因未诊断 |
| T+12:00:00 | 完整全局最优性证明仍缺，原测试失败 |
| 截止以后 | 状态管理及独立请求的报告／发布，未恢复数学求解 |
WSL 故障确实中断计算，但故障前仍无完整证明，不能据此推断环境正常必能按时完成。
### 事后候选指纹核对
本次发布整理单独运行最新私有源码所配公开协议 `diskcover-minpoly-v1`：使用原部分交付的候选最小多项式和目标根，以**精确有理二分、整数符号判断及整数舍入**认证半径 20 位小数的 ROUND_HALF_UP 结果，再计算规范 UTF-8 JSON 的 SHA-256。精确区间两端舍入到同一 20 位值，没有使用未经控制的浮点近似。
计算结果：`2cf89430e0f746fabd1f84298f3449cb9f755a8c3d41a198b2881dd042d06e12`。
**与 n25 参考指纹一致。** 原发布将参考标为 `candidate_upper_bound`；2026-10-03 根据 2026-09-26 已接受的项目本地全局最优性复核更正该标记。原 Astra 测试在截止时仍未交付完整全局证明，成绩保持 0 分。指纹匹配不验证提交证明；半径、系数和隔离端点仍不公开。
### 验证、交付与限制
原交付保存候选代数、解析覆盖、较弱普遍下界及局部证书，缺少全局排除链。原部分证明 ZIP 共 37 项，内部 36 项 manifest 的 SHA-256 及 ZIP CRC 在前次报告整理中检查，零不匹配；本次未重新完整重放数学证明。原包 SHA-256：`892ed4ee2a545d673dc719579484abaa45fe0e2525037dbc84a76cb8db3bcb5a`。
本次新增的是精确指纹计算、失败计分脚本执行和网站构建发布检查。它们不能替代原题证明。网页仅发布报告、原用户输入、机器可读记录和指纹；私有证明及选定运行证据保留在本地，选定证据包不是完整聊天档案。原报告与证据保持原字节，本次作为后续公开版本保存。
## 可下载记录
[本次测试的机器记录](record-n25-astra-20261002.json) · [本报告 Markdown](record-n25-astra-20261002.zh.md)
# n=25 · gpt-6 astra/max 测试报告
[返回 n=25](n25.zh.html) · [测试记录目录](records.zh.html)
**成绩：0（未完成）。** 测试发生于 2026-10-02（UTC），原限时 12 小时。截止时缺少对任意圆心构型成立、与候选半径匹配的全局下界，没有完成原题。测试编号：`T_20261002T095207Z_01a0fc07`。原模型由截止前 12 条运行上下文核实为 gpt-6-astra / max；事后整理阶段另为 gpt-6.1-sol / xhigh。
## 25圆覆盖6.1 sol vs 6 astra实验结果分析
这次25圆覆盖测试，Sol 的表现确实超出我的预期。实验前我的预期是，这道题对两个模型都是第一次很难做出来的问题，即运行12小时最终得0分。Astra/Max的测试结果的确符合我的预期，但是 GPT‑6.1 Sol/Max 在五小时左右完成了证明，最终得分230分，这让我感到意外。于是我想弄清楚：Sol 到底做对了什么，为什么它能快这么多？
我最初怀疑，差别可能主要在资料检索。Sol 很早就找到了一个公开的20圆覆盖项目，其中有完整证明和程序，可以作为25圆问题的基础。于是我又做了一次对照实验，把相关资料和迁移方向的提示直接放进 prompt，让 Astra 参考。这一次我的预期是，既然不需要再自己找资料，Astra 应该有机会在五小时左右，甚至更短的时间里完成。
结果第二次 Astra 到七小时多被中断时，依然没有完成。
### 证明的难点
这道题要用至多25个全等小圆盘覆盖整个闭单位圆盘，求出最小的共同半径，严格证明它最优，再给出这个代数数的最小多项式。最优半径的最小多项式只有四次，所以最复杂的部分则是证明这些圆盘确实覆盖了目标圆盘，并且半径不能再小。
Sol 先按圆心之间的相邻关系，把需要考虑的覆盖归纳成有限种结构，再逐类排除可能用更小半径完成覆盖的情况。结构数量很多，每种结构下又有无穷多种圆心摆法，排除这些可能性需要大量计算。要节省时间，就需要一个或多个检查成本低、又能排除大量可能性的条件：只要能严格证明某类结构或某批分支不可能产生更好的覆盖，就可以整体跳过，不再继续计算其中的具体情况。能否较早找到并用好这样的条件，会是影响证明速度的关键。
### 从20圆的证明，做出25圆的证明
最初看到 Sol 的结果时，我怀疑它的证明是不是错了。我用已有的研究资产反复核对以后，确认这份证明是对的。那么，它到底怎么做到的？
仔细分析实验数据后发现，Sol 在开始十几分钟后，找到了 GitHub 上公开的20圆覆盖完整证明。它参考其中的推导和程序，搭起了25圆覆盖的证明框架，然后继续研究怎样减少需要排除的结构。约1小时53分和2小时51分时，两个检查成本很低的排除条件已经先后用进了程序。
这两个条件能排除大量不可能的结构。有些分支还没生成完整的图，就已经能确定不满足条件，可以直接删掉。后面原本要针对这些分支做的计算，也就一起省了下来。Sol 借鉴了20圆的证明，又找到了适合25圆问题的办法，最后在五小时左右完成，得了230分。
### Astra 只是运气不好吗？
第一次 Astra 跑了整整十二小时，最终得0分。它有候选覆盖，也有局部证明和几何结论，但始终没有完成全局最优性的证明，也没有找到并用好同样高效的一组排除条件。
不过，这时我还没有认定 Astra 的能力就比 Sol 差。因为Sol 很早找到了那份20圆覆盖证明，而第一次 Astra 的公开执行记录中，却没有看到它找到或参考这份资料。因此，我当时怀疑：差距会不会主要来自资料检索？
于是我设计了一个对照实验：控制goal prompt整体不变，只是把资料对应的github链接直接给 Astra，并明确让它也参考那份证明，再做一次。
### 把参考资料给 Astra，再测一次
对于这次对照实验，我的预期是，既然资料已经摆在面前，Astra 不需要自己找，应该有机会比 Sol 更快。结果它确实参考了资料，也很快搭起了相近的证明框架，但后面的工作依旧没有完成。
Sol 在不到五小时的计分用时内就完成了任务，Astra 却到约5小时50分才明确提出第一个排除条件，随后证明并投入计算。直到约7小时10分38秒实验中断，它仍未完成全局证明；记录中也没有看到第二个条件被完整推出并用于排除。第一个条件来得晚，第二个条件还没完整用上实验就结束了。
所以，给出资料和迁移提示以后，Astra 仍然没有追上 Sol。第一次是十二小时未完成；第二次是七小时多停止时仍未完成。
### 这一局，Sol 赢了
对照实验之后，我原先那个“可能只是运气不好，没搜到资料”的解释，就不够了。资料已经给了，Astra 也参考了，结果还是没有做完。
Sol 那次做得好的地方，是能把20圆的证明迁移到25圆，较早找出低成本的排除条件，并把它们用于计算。这些条件让它省掉了大量工作。Astra 即使拿到了同样的参考资料，也没能及时做到这一步。从这几次25圆覆盖的表现来看，Astra 明显输给了 Sol。我已经给了它第二次机会，结果还是如此。
至于所有数学研究中 Sol 是否都强于 Astra，这几次实验回答不了。
### 三次实验的成绩与参考资料
| 测试 | 参考资料 | 结果 |
|---|---|---|
| GPT‑6.1 Sol/Max | 未预先提供上述两组针对性资料，自行检索 | 230分；计分用时4小时52分19秒，最终聊天答复约5小时05分 |
| Astra/Max 首次 | 未预先提供上述两组资料 | 0分；十二小时截止时未完成全局最优性证明 |
| Astra/Max 参考材料实验 | 明确提供通用理论、20圆完整证明和程序，并提示迁移 | 约7小时10分38秒中断时未完成；未登记网页成绩 |
首次 Astra 的0分表示限时内没有完成全部证明，不代表它已有的局部结果全部错误。第二次没有运行满十二小时，也没有登记网页成绩。Sol 的230分沿用已有测试审核结果。
对照实验提供的材料固定在实验前已有的公开版本，包括[通用精确算法理论](https://github.com/VonEquinox/DiskCoveringSolve/blob/089584973f41e6374ce110f6e5b5ee456df19352/theory/single_exponential_exact_algorithm_zh.md)、[20圆完整证明](https://github.com/VonEquinox/DiskCoveringSolve/blob/089584973f41e6374ce110f6e5b5ee456df19352/cover20/docs/r20_proof_zh.md)和[20圆程序包](https://github.com/VonEquinox/DiskCoveringSolve/tree/089584973f41e6374ce110f6e5b5ee456df19352/cover20/proof_bundle)。已发布的成绩说明见[Sol 测试报告](https://pikaaa345.github.io/disk-covering-benchmark/record-n25-sol-20261002.zh.html?lang=zh)和[首次 Astra 测试报告](https://pikaaa345.github.io/disk-covering-benchmark/record-n25-astra-20261002.zh.html?lang=zh)。
## 测试报告详情
### 已有结果的来源与本次模型工作
原运行通过 [Friedman 圆覆盖表](https://erich-friedman.github.io/packing/circovcir/)取得已知 25 圆盘候选，原交付将构型归于 Jeremy Tan（2018）。本次模型整理了候选精确代数数据、整个闭圆盘的解析覆盖论证、较弱普遍下界和限定邻域的局部证书，并尝试全局排除。
**没有取得或完成 n=25 的完整全局最优性证明。** 与 n=11 历史报告复用外部完整证明材料的条件不同，候选覆盖、局部最优性和全局最优性分别判断；不能把既有候选或局部证书描述为完成原题。
### 任务与时间
| 口径 | 记录 |
|---|---|
| 原测试起点 | 2026-10-02 09:52:07 UTC，Goal 创建 |
| 原截止 | 2026-10-02 21:52:07 UTC，包含截止时刻 |
| 展示评测窗口 | **12 小时（43200 秒）**；失败观察窗口，不是成功完成用时 |
| 有效完成用时 | null；未得到完整有效结果 |
| 已保存 Goal 系统累计耗时 | 11 小时 38 分 50 秒（41930 秒）；含截止后管理续行，不替代自然时间 |
| 失败答复 | message create_time 约 T+12:00:39；JSONL 写入约 T+12:01:08，两者均不是成功完成端点 |
| 原报告证据冻结 | 2026-10-03 01:04:39.748 UTC，即 T+15:12:33；包含等待及另行报告任务，不延长原预算 |
| 原报告整理阶段 | 请求至该冻结节点约 22 分 51 秒；不含随后打包、归档及本次发布 |
未完成先记 0 分，不把使用 12 小时换算为成功完成效率。系统计时和自然时间分别保存；并行程序耗时不再相加。后续哈希核对、报告整理与发布不计入原测试的有效完成时间。
### 计算条件
| 项目 | 记录 |
|---|---|
| CPU | AMD Ryzen 9 8945HX with Radeon Graphics |
| 内存 | DDR5，32 GB；总容量 34359738368 字节 |
| 配置证据 | 原报告整理时 Windows CIM 查询，不是开题硬件快照 |
| 执行位置 | 本机 Ubuntu WSL；可见证据没有关键远程计算 |
| 软件 | 原包记载 Python 3.12.3、SymPy 1.14.0；未核实 Sage 或 Wolfram 实际求值 |
| 临时工具 | 公开取得 CaDiCaL 1.9.5、drat-trim（版本未知），没有完成全局不可满足证书 |
428 条截止前去重 response usage：输入 58,597,430，其中缓存输入 55,492,736；输出 905,374，其中推理输出 561,373；合计 59,502,804。最后保存节点约 T+11:59:38，可能缺少截止时仍在进行的请求。缓存和推理均为对应总量的子集，不能再次相加。Goal 自身计数 3,906,233 属不同范围，含事后管理续行。费用未取得账单，记 null。
### 输入提示词
原用户要求读取 n25 中文网页的测试 Prompt。限制为：**不得读取测试前已有本地资料、技能、其他聊天或归档聊天，以及 WSL 中已存研究资料；允许公开网络和 WSL 工具；12 小时内须得到完整且正确的结果。** 数值优化、浮点结果、有限采样、边界检查、图像或尚未完成的枚举不能代替完整证明。
[下载当时实际发送的原始用户输入](reports/n25-astra-main-prompt.original.txt)。保存的是原 Goal 的 objective 字段；没有开题时网页字节快照，因此不把今日题面冒充历史原文。
<details><summary>展开原题要求的可核实摘要</summary>
令 $D=\{x\in\mathbb R^2:\|x\|_2\le1\}$，
$$R_D(C)=\max_{x\in D}\min_{1\le i\le25}\|x-c_i\|_2,\qquad r_D(25)=\inf_{C\in(\mathbb R^2)^{25}}R_D(C).$$
要求确定 $r_D(25)$，列出目标半径的本原不可约整系数最小多项式、有理隔离区间及唯一根证明；给出唯一指定的有序代数圆心；严格证明整个闭圆盘覆盖；证明任意 25 圆心构型均不能更优，未经证明不能限定对称性或组合结构，须覆盖退化情形。使用计算机辅助证明须交付实际代码、输入、证书与验证材料。仅存在性、代数性、算法或候选不视为完成。
这是原指令、原成果和报告中可核实的要求摘要，不是开题网页原字节转录。原求解禁令不由事后报告的本地访问授权追溯改变；本次未进行全面合规审计，评分由未完成已充分决定。
</details>
### 主要阶段
以原 Goal 创建为 T+00:00:00；以下为保存的进度／工具节点，不推定首次发现时刻，也不是互斥 CPU 时间。
| 相对自然时间 | 主要工作与状态 |
|---|---|
| 约 T+00:04:08—00:04:43 | 公网检索候选来源和 Friedman 表；未找到 n25 完整全局证明 |
| 约 T+00:44:15—00:46:49 | 较弱下界算术检查与第一版部分交付；候选代数、全盘覆盖有材料，全局下界缺失 |
| 随后截止前研究 | 48 个局部必要约束、精确驻点与 Taylor/Loewner 余项证书；全局搜索未完成 |
| 约 T+10:19:49—10:43:10 | 限定邻域局部整数证书及独立核验日志；未把任意构型归入该邻域 |
| 约 T+11:35:28 | 4,719,313 条 SAT 输入子句检查通过，程序约 433 秒；明确标记 NOT_GLOBAL_UNSAT |
| 约 T+11:44:51—11:54:20 | WSL 出现 E_UNEXPECTED、Stopped 和 CreateInstance/E_FAIL，末段计算中断；原因未诊断 |
| T+12:00:00 | 完整全局最优性证明仍缺，原测试失败 |
| 截止以后 | 状态管理及独立请求的报告／发布，未恢复数学求解 |
WSL 故障确实中断计算，但故障前仍无完整证明，不能据此推断环境正常必能按时完成。
### 事后候选指纹核对
本次发布整理单独运行最新私有源码所配公开协议 `diskcover-minpoly-v1`：使用原部分交付的候选最小多项式和目标根，以**精确有理二分、整数符号判断及整数舍入**认证半径 20 位小数的 ROUND_HALF_UP 结果，再计算规范 UTF-8 JSON 的 SHA-256。精确区间两端舍入到同一 20 位值，没有使用未经控制的浮点近似。
计算结果：`2cf89430e0f746fabd1f84298f3449cb9f755a8c3d41a198b2881dd042d06e12`。
**与 n25 参考指纹一致。** 原发布将参考标为 `candidate_upper_bound`；2026-10-03 根据 2026-09-26 已接受的项目本地全局最优性复核更正该标记。原 Astra 测试在截止时仍未交付完整全局证明，成绩保持 0 分。指纹匹配不验证提交证明；半径、系数和隔离端点仍不公开。
### 验证、交付与限制
原交付保存候选代数、解析覆盖、较弱普遍下界及局部证书，缺少全局排除链。原部分证明 ZIP 共 37 项，内部 36 项 manifest 的 SHA-256 及 ZIP CRC 在前次报告整理中检查，零不匹配；本次未重新完整重放数学证明。原包 SHA-256：`892ed4ee2a545d673dc719579484abaa45fe0e2525037dbc84a76cb8db3bcb5a`。
本次新增的是精确指纹计算、失败计分脚本执行和网站构建发布检查。它们不能替代原题证明。网页仅发布报告、原用户输入、机器可读记录和指纹；私有证明及选定运行证据保留在本地，选定证据包不是完整聊天档案。原报告与证据保持原字节，本次作为后续公开版本保存。
## 可下载记录
[本次测试的机器记录](record-n25-astra-20261002.json) · [本报告 Markdown](record-n25-astra-20261002.zh.md)