用Lean 4自动验证数学定理是否新颖，突破仅验正确性的局限。
Beyond Correctness: Toward Automated Novelty Verification with Lean 4
- 通过形式化论文内容，结合三维度判断新颖性：已有定理存在性、证明非平凡性、前提集结构距离。
- 在撤稿论文上验证，发现编译通过不等于语义一致，且索引覆盖是主要瓶颈。
- 适合数学自动化验证、AI辅助科研者，尤其关注定理新颖性检测的场景。
将AI应用于数学时，现有系统仅能验证定理正确性，无法判断其是否为新成果：一个在Lean中无错误编译的定理可能已是已知结果。本文提出AViD Journal流程，接收LaTeX论文，将其命题形式化为Lean 4代码，并通过决策树在三个维度判断新颖性：形式化知识库（Mathlib）与非形式化知识库（TheoremSearch和Matlas）中的已有性（含时间过滤与LLM判别）、通过自动策略验证证明非平凡性、以及基于前提集的杰卡德距离衡量证明结构差异。在因重复声明而从arXiv撤稿的论文上评估，结果揭示了三项限制：第一，成功编译不代表语义忠实；第二，召回率受限于定理索引覆盖率，而非相似度度量；第三，arXiv撤稿后删除源码，损害基于此类论文的基准可复现性。
原文摘要 · Abstract (English)
Artificial intelligence systems applied to mathematics verify correctness but not novelty: an automatically generated theorem can compile in Lean without errors and yet be an already known result. This article presents AViD Journal, a pipeline that receives a LaTeX article, formalizes its statements in Lean 4, and issues a novelty verdict through a decision tree over three dimensions: prior existence in a formal corpus (Mathlib) and an informal one (TheoremSearch and Matlas, with temporal filter and LLM judge), non-triviality via automatic tactics, and structural distance between proofs measured as Jaccard distance over premise sets. Evaluation on papers withdrawn from arXiv due to declared duplication produced a result more informative than any performance measure: the identification of three obstacles that limit the approach regardless of this implementation. First, successful compilation of a Lean file does not guarantee semantic fidelity. Second, the recall ceiling is imposed by the coverage of theorem indices, not by the similarity metric. Third, arXiv removes the source code of articles upon withdrawal, compromising the reproducibility of any benchmark built upon them.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。