Sol 6.1 (xhigh)
模型详细评测 · 公开＋私有合并成绩
当前成绩
内容可靠率与目标达成率
已审内容可靠率 98.93%；已确认目标达成率 82.61%。
| 子类 | 已审内容可靠率 | 已确认目标达成率 |
|---|---|---|
| 书面论证 | 100.00% | 100.00% |
| 论证审阅 | 100.00% | 92.50% |
| 语义审计 | 100.00% | 100.00% |
| 形式化 | 100.00% | 91.30% |
| 对齐自查 | 90.00% | 66.67% |
| 背景核查 | 100.00% | 100.00% |
| 数学想法手稿化 | 100.00% | 80.00% |
| 命题拓展 | 100.00% | 0.00% |
分类贡献
贡献分 / 该项满分；相关变体在家族内聚合。
Lean · 自查计分
比较三种计分口径
整章对齐 · 固定三轮
展开三轮原答与审核
R1 · 完整原答
FULL
上一版未完成全部要求。本版补齐原有 12 项缺项，并补充熵差的正、负无穷分支。全部 92 项均已完成；整合源码通过指定 Lean 4.29.1 编译，223 个自建声明的公理审计仅包含 propext、Classical.choice、Quot.sound。未修改冻结背景。
数学来源：Zhe Li（Glen Li / glenzli），The Operator Evolution Theory，CC BY 4.0。以下为新增形式化。
import Lake
open Lake DSL
package «mg-c003»
require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @
"5e932f97dd25535344f80f9dd8da3aab83df0fe6"
lean_lib Frozen where
roots := #[]
globs := #[.submodules `formal_oet]
@[default_target] lean_lib Main where
roots := #[`Main]
leanprover/lean4:v4.29.1
查看原始记录 ↗View original record ↗查看原始记录 ↗View original record ↗R2 · 完整原答
FULL
发现并修复了一处量词对齐缺口：原有限纤维链两项引用了要求无限序列逐步包含的定理。本版新增直接针对 Fin (m+1) 有限链的证明，包含零步边界及端点真包含的差集见证，并更新对应对齐记录。
92 项均为 complete。整合源码在指定编译器及 mathlib 提交下重新编译通过；227 个自建声明的公理审计仅涉及 propext、Classical.choice、Quot.sound。Lake 构建配置检查通过。未修改原始规格或冻结背景。
数学来源：Zhe Li（Glen Li / glenzli），The Operator Evolution Theory，ORCID，CC BY 4.0。以下为新增形式化。
import Lake
open Lake DSL
package «mg-c003»
require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @
"5e932f97dd25535344f80f9dd8da3aab83df0fe6"
lean_lib Frozen where
roots := #[]
globs := #[.submodules `formal_oet]
@[default_target] lean_lib Main where
roots := #[`Main]
leanprover/lean4:v4.29.1
查看原始记录 ↗View original record ↗查看原始记录 ↗View original record ↗R3 · 完整原答
KEEP
本轮未发现需要修复的缺陷，维持上一版 92 项 complete。上一版答卷主体及全部命名文件按原字节继承。
核查依据：
- 92 个义务 ID 完整覆盖、无重复；声明引用均实际存在。
- 六个冻结背景模块及
Main.lean重新编译通过；编译器与 mathlib 提交符合规格。 - 227 个自建声明的递归公理审计仅涉及
propext、Classical.choice、Quot.sound。 - Lake 配置检查通过；复核了空域、零步链、无穷距离、开球端点及熵差良定性。
- 提交文件与冻结背景均未改动。
仍有的不确定性是中文原文与 Lean 命题之间的人工语义对齐判断；编译和公理审计无法自动认证这种对应。本轮核对未发现遗漏或偏差。
92项义务，按最后规定轮次计分。
公开题 · 逐题成绩与证据
公开25题；私有14题计入合并成绩。
形式化初答 · 逐题核实数
按初答封卷工程核对编译及语义对应。
可靠性审核
公开题的错误承诺与扣罚理由
同根因扣罚去重；具体依据见逐题说明。
Harness与工具
Codex CLI
39道初答及三轮自查实际执行338个本地命令；允许本地文件、计算与预置公共依赖，禁止工具联网。
运行版本与来源
本批次使用Codex CLI，以xHigh请求；42次物理请求均为首答，无重试或系统排除。后端型号与effort未回显，保持未知。