发表机构
Institut Supérieur de Gestion, Université de Tunis（突尼斯大学高等管理学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究指出机器检查使数学验证变得丰富但裁决稀缺，区分了验证的三个层次，通过测量成果集说明负担转移，并提出相关分类法、披露方案及应用启示。
AI 中文摘要
2026年5月，一个OpenAI模型给出了厄尔多斯单位距离猜想的反例。当天有五位数学家发表了人类验证的版本，该结果在数周内被纳入文献。2026年8月，同一家实验室发布了10项数学及理论计算机科学成果，每项成果都附带了无未证明步骤的机器可验证Lean 4证书。四周后，其中一项成果成为关于其形式化是否符合其主张的未解决争议的主题。我们认为这种差异是结构性的。我们区分三个验证层次：核心（kernel）检查的推导有效性、形式陈述是否表示预期问题的表示保真度，以及认知意义。只有第一个层次是可机械化的。因此，使其实际上免费并不会消除验证工作，而是将负担转移到依赖稀缺专家关注的层次。对8月成果集的测量说明了这种转移：核心检查的证明总计20.6 MB，而需要人工审核的陈述总计55.6 KB，比例为379比1。然而这些陈述包含218个定制定义，而非依赖经社区审核的定义。因此，审核表面在体积上很小，但不可避免地需要专家参与。我们认为机器检查产生了验证丰富性，同时保留了裁决稀缺性。我们提出了一个表示不匹配的六类别分类法、一个针对机器生成数学主张的披露方案，以及对软件、密码学和受监管决策系统的启示。
英文摘要
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.
