OpenAI Result 198 的 every-field refinement 获独立 Lean 4 formalization：58 个 targets 通过 28 组 Comparator

Qiyue Tang 在基于 OpenAI Result 198 的 refinement 工作中，把 infinite little finitistic dimension 的构造简化并扩展到 every field；10 月 10 日进一步公开 Note198-formalization。项目固定 Lean 4.34.1 / Mathlib 依赖，对列出的 58 个 targets 运行 28 个 Comparator groups，接受目标的依赖只出现 propext、Classical.choice、Quot.sound 且无 sorryAx，并保存 verification logs / receipts。上游研究过程披露先由 GPT-6 Astra Pro 做 adversarial review 与 strengthening，再由独立 GPT-6 Astra 再审；Lean 仓库则明确说明 AI 用于形式化准备与 proof review。项目同时说明 formalization 覆盖的是列出的目标，不声称逐句覆盖整篇 manuscript，也不把机器 verification 等同于 human verification。