Sol 6.1 (max)
模型详细评测 · 公开＋私有合并成绩
当前成绩
内容可靠率与目标达成率
已审内容可靠率 99.90%；已确认目标达成率 90.92%。
| 子类 | 已审内容可靠率 | 已确认目标达成率 |
|---|---|---|
| 书面论证 | 100.00% | 100.00% |
| 论证审阅 | 100.00% | 92.50% |
| 语义审计 | 100.00% | 100.00% |
| 形式化 | 100.00% | 100.00% |
| 对齐自查 | 100.00% | 100.00% |
| 背景核查 | 100.00% | 100.00% |
| 数学想法手稿化 | 99.00% | 100.00% |
| 命题拓展 | 100.00% | 16.67% |
分类贡献
贡献分 / 该项满分；相关变体在家族内聚合。
Lean · 自查计分
比较三种计分口径
整章对齐 · 固定三轮
展开三轮原答与审核
R1 · 完整原答
KEEP
本轮未发现需要修复的缺陷，维持上一版全部交付及 92 项 complete 标记。答卷主体、全部命名文件和对齐表原字节继承，原始规格与冻结背景未改动。
核查依据：
- 在指定 Lean 版本及固定 mathlib 环境中，全项目重新编译通过。
- 92 个义务 ID 恰好覆盖，无重复或遗漏；219 个不同映射声明均存在于指定模块。
- 重新提取声明依赖，与对齐表一致。
- 公理审计覆盖 482 个本章声明，仅涉及
propext、Classical.choice、Quot.sound。 - 逐项复核了空域因子化、实际中间像域、严格半径边界、零与无穷情形，以及习题的内部中心和覆盖数分段端点。
仍有的不确定性：编译与公理审计验证 Lean 声明及其证明；原文与这些声明的语义对应仍依赖逐项审阅，不能据此保证“100% 绝无错配”。本轮审阅未发现此类问题。
R2 · 完整原答
KEEP
本轮未发现需要修复的缺陷，维持全部 92 项 complete。答卷主体、全部命名文件及对齐表原字节继承；原始规格与冻结背景未改动。
本轮实际核查依据：
- 全项目在指定 Lean 编译器及 mathlib 提交下重新编译通过，仅有 lint 警告。
- 92 个义务 ID 完整覆盖，无重复；219 个映射声明均存在于指定模块。
- 从重新编译的声明中提取依赖，逐声明核对结果与对齐表一致。
- 482 个本章声明及所映射背景声明的递归公理审计通过，仅涉及
propext、Classical.choice、Quot.sound。 - 逐项复核了空域因子化、实际中间像域、常值优先、严格半径边界、零与无穷分支，以及全部习题的构造、内部中心和覆盖数端点。
仍有的不确定性：编译和公理审计不能自动证明自然语言原文与 Lean 声明完全对应。本轮语义审阅未发现遗漏或错配，但不能将这一审阅结果表述为“100% 绝无缺陷”的形式化保证。
R3 · 完整原答
KEEP
本轮未发现需要修复的缺陷，维持全部 92 项 complete。上一版答卷主体、全部命名文件和对齐表原字节继承；原始规格与冻结背景未改动。
本轮实际核查依据：
- 编译器完整提交号、mathlib 提交号均与规格一致；全项目重新编译通过，仅有 lint 警告。
- 92 个义务 ID 恰好覆盖；219 个映射声明均存在于指定模块。
- 重新提取声明依赖，与对齐表逐项比对，差异为零。
- 482 个本章声明及 6 个映射背景声明的递归公理审计通过，仅涉及允许的三项逻辑公理。
- 复核了实际中间像域、空域因子化、常值优先、严格半径边界、零与无穷分支，以及习题的构造合法性、内部中心和覆盖数端点。
仍有的不确定性：编译和公理审计验证的是所写 Lean 命题；自然语言原文与形式声明的完整对应仍依赖语义审阅。本轮未发现错配，但这些检查不能提供“100% 绝无缺陷”的保证。
92项义务，按最后规定轮次计分。
公开题 · 逐题成绩与证据
公开25题；私有14题计入合并成绩。
形式化初答 · 逐题核实数
按初答封卷工程核对编译及语义对应。
可靠性审核
公开题的错误承诺与扣罚理由
同根因扣罚去重；具体依据见逐题说明。
Harness与工具
Codex CLI
39道初答及三轮自查实际执行438个本地命令；允许本地文件、计算与预置公共依赖，禁止工具联网。
运行版本与来源
本批次使用Codex CLI，以Max请求；42次物理请求均为首答，无重试或系统排除。后端型号与effort未回显，保持未知。