A new tool checks whether a proven theorem is actually new, not just error-free.
Researchers built AViD Journal, a pipeline that takes a LaTeX math paper, formalizes its statements in Lean 4, and runs a decision tree to judge novelty. It checks three things: whether the result already exists in a formal database (Mathlib) or informal ones (TheoremSearch and Matlas, filtered by date and an LLM judge), whether the proof is trivial to derive with automatic tactics, and how structurally different it is from known proofs, measured by Jaccard distance over the underlying premises. The team tested it on papers withdrawn from arXiv for duplication.
This matters because Lean and similar proof assistants solved the wrong half of the problem. They confirm a proof is logically valid, but say nothing about whether anyone proved it first. As AI systems churn out more machine-checked math, that gap becomes a real risk: a model could "discover" something already sitting in a textbook, and compilation alone would wave it through.
The paper is refreshingly honest about what it doesn't solve. A Lean file compiling doesn't mean it faithfully captures the original claim. Novelty detection can only be as good as the theorem indexes it searches, so recall is capped by database coverage, not by the matching method. And arXiv deletes source code from withdrawn papers, which quietly undermines the reproducibility of any benchmark built on them - including, presumably, this one.