OpenAI 数学猜想证明手稿的六条命题完成 Lean 形式化

OpenAI 一份模型生成的数学研究手稿中，六条主要命题已在 Lean 形式化数学系统中完成形式化。读者可用开源工具 Comparator 验证，证明仅依赖三条标准公理；目前尚无专家公开评估其完整性与正确性。