OpenAI 的十个数学结果：Lean 证书查得通，谁审的那一栏写着 agent
十份 Lean 证书、零个 sorry、三条标准公理，还配了对抗式复核工具。分水岭不在证明对不对，而在 formalization.yaml 里 review.status 写的是 agent-reviewed。
标签
标签
十份 Lean 证书、零个 sorry、三条标准公理，还配了对抗式复核工具。分水岭不在证明对不对，而在 formalization.yaml 里 review.status 写的是 agent-reviewed。