OpenAI Codex 实质参与 Dimitrov Conjectures 1 和 3 的 proof discovery，并发布 Lean 4 全参数范围形式化

Michael Mazur 9 月 13 日发布 Dimitrov Conjectures 1 和 3 的 Lean 4 形式化。公开仓库称 OpenAI Codex 在其指导下承担了 substantive target selection、proof discovery、literature searching、Lean formalization 与 documentation。形式化覆盖所有自然数 k≥1、n≥2，并给出 equality iff n is prime；`Solution.lean` 无 sorry 或 custom axiom，仓库提供 `lake build`、`--trust=0`、Comparator 与 NanoDa replay。项目同时明确不声称历史首证，priority 尚未获得源论文作者或独立专家确认。