AI systems for mathematics check whether a theorem is correct but not whether it is new. A generated theorem can compile in Lean and still be an already known result. Equating novelty with absence from Mathlib is a poor criterion: it flags trivial facts as new and misses results that exist only in the informal literature.

AViD Journal parses a LaTeX article, orders its theorem environments by their dependencies, and formalizes them in Lean 4 using one of several selectable LLM backends. A decision tree with eight possible verdicts then checks three dimensions. The first is prior existence in Mathlib (searched via Leandex) and in the informal TheoremSearch and Matlas indices, using a temporal filter and an LLM judge. The other two are non-triviality, tested by whether automatic tactics such as aesop, decide or norm_num close the goal, and proof distance, measured as Jaccard distance over premise sets. Each instrument is validated separately, and the whole pipeline is evaluated on arXiv papers withdrawn for declared duplication, each paired with matched controls.

The Jaccard distance was consistent with the human judge on 5/5 calibration pairs, and the triviality check succeeded on 22/24 cases. Backend choice mattered: Qwen 3.7-max formalized 5/5 test cases while both DeepSeek models formalized 0/5. The evaluation identified three obstacles that limit the approach regardless of implementation: successful compilation does not guarantee semantic fidelity, recall is capped by the coverage of theorem indices rather than the similarity metric, and arXiv removes the sources of withdrawn papers, undermining reproducibility of such benchmarks.