OpenAI Codex 实质参与证明 Collatz predecessor 的正下密度定理，并由 Lean 4 完整检查

Lech Mazur 证明：对任意固定正整数目标 a 且 3∤a，普通 Collatz 迭代中最终到达 a 的正整数集合具有正下自然密度。ProofAtlas 明确记录 OpenAI Codex 对 computation、proof strategy、formalization 与 exposition 有 substantial contribution；公开 Lean artifact 通过 build，三个主定理根无 unfinished proof。结果还推出：若存在一个正整数永不到 1，则不收敛集合具有正下密度；而 upper-natural-density-one convergence 会推出所有正整数最终到达 1。后者的 density-one 前提并未被证明。