OpenAI模型提出数学猜想反例，机器检查证明与人工验证的冲突揭示了数学验证的新挑战。
OpenAI模型在2026年5月提出了Erdős单位距离猜想的反例，同一日有五位数学家发布了人工验证版本。同年8月，该实验室发布了10个数学和理论计算机科学成果，每个都附带无未证明步骤的Lean 4机器可检查证书。四周后，其中一个结果仍存在关于其形式化是否意味着其所声称内容的未解决争议。研究指出，机器检查产生了验证丰富性，但裁决仍然稀缺。
Verification abundance, adjudication scarcity: what happens to mathematical knowledge when proof checking becomes free
In May 2026 an OpenAI model produced a counterexample to the Erdős unit distance conjecture. Five mathematicians published a human-verified version the same day, and the result entered the literature within weeks. In August 2026 the same laboratory published ten mathematical and theoretical computer science results, each accompanied by a machine-checkable Lean 4 certificate with no unproved steps. Four weeks later, one remained the subject of an unresolved dispute over whether its formalization meant what it claimed. We argue that this difference is structural. We distinguish three layers of verification: derivational validity, which a kernel checks; representational fidelity, whether the formal statement means the intended question; and epistemic significance. Only the first is mechanizable. Making it effectively free therefore does not eliminate verification work but shifts the burden to layers dependent on scarce expert attention. Measurements of the August corpus illustrate the shift. The kernel-checked proofs total 20.6 MB, while the statements requiring human audit total 55.6 KB, a ratio of 379 to 1. Yet those statements contain 218 bespoke definitions rather than relying on community-vetted ones. The audit surface is therefore small in volume but irreducibly expert. We argue that machine checking produces verification abundance while leaving adjudication scarce. We propose a six-category taxonomy of representational mismatch, a disclosure schema for machine-generated mathematical claims, and implications for software, cryptography, and regulated decision systems.