Beyond Correctness: Toward Automated Novelty Verification with Lean 4

Ayrton Porto

Source-linked AI summary

Beyond Correctness: Toward Automated Novelty Verification with Lean 4

Ayrton Porto

arXiv:2608.14669v1Aug 2, 2026cs.AI

TL;DR

AI systems can verify mathematical correctness without establishing whether results are novel. AViD Journal formalizes LaTeX articles in Lean 4 and issues novelty verdicts, revealing corpus coverage and semantic-fidelity obstacles that constrain detection.

Problem
Existing systems can generate compiling proofs without systematically assessing whether the underlying mathematical result is genuinely new.
Method
AViD Journal extracts mathematical statements from LaTeX, formalizes them in Lean 4, and applies a three-dimensional decision tree for novelty verdicts.
Results
The evaluation found that absent detections were determined by the pre-electronic age of duplicating results rather than the metric or language-model judge.
Takeaways & Limitations
The framework measures novelty only over statements and proofs frozen in indexed corpora, not the conceptual novelty of definitions or transferable methods.
Takeaways & Limitations
Statement comparison is syntactic, while formalizing third-party proofs succeeded in 0% of the proof-of-concept cases, limiting downstream comparison.

Abstract

from arXiv · show

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.

1 Introduction

The paper argues that mathematical AI can produce Lean-correct results that are nevertheless non-novel, while Mathlib-only novelty checks both overestimate trivial results and miss informal prior work. It introduces AViD Journal, a pipeline that formalizes LaTeX statements in Lean 4 and evaluates novelty across formal and informal prior existence, non-triviality, and proof structure, with evaluation centered on three implementation-independent obstacles.

Problem: Mathematical AI systems verify correctness but not novelty, and compilation alone does not establish that a generated result is new.The paper identifies prior-proof reuse and the gap between syntactic compilation and genuine novelty as central problems.
Problem: A Mathlib-only novelty criterion both labels tactic-trivial theorems as new and misses results published only in informal literature.These failures motivate combining formal-corpus search with informal-literature search and non-triviality checks.
Contribution: AViD Journal converts a LaTeX article into Lean 4 formalizations and produces an eight-verdict novelty decision using three dimensions.The dimensions cover prior existence in Mathlib, TheoremSearch, and Matlas; non-triviality via automatic tactics; and proof distance via Jaccard distance over premise sets.
Evaluation: The evaluation benchmarks papers withdrawn from arXiv for declared duplication against category- and year-matched controls, including duplicator retrievability.The benchmark is designed to assess whether prior duplicated results can be recovered from available sources.
Limitations: The evaluation characterizes three walls: Lean compilation may lack semantic fidelity, duplicated results may predate available corpora, and withdrawn arXiv papers lose their LaTeX source.Together, these obstacles limit fidelity, recall, and reproducibility independently of the implementation.

2 Related Work

Prior work supplies theorem search, Lean formalization, non-triviality filtering, and proof-similarity infrastructure, but AViD composes these components into a LaTeX-to-verdict pipeline for automated novelty verification. Its distinctive contribution is the decision layer combining formal and informal corpus searches, temporal filtering, non-triviality checks, and structural proof comparison.

Informal theorem search: TheoremSearch and Matlas provide complementary informal coverage, spanning arXiv since 1991 and peer-reviewed journals since 1826, which AViD uses as two corpus branches.TheoremSearch indexes 9.2 million statements, while Matlas contains 8.07 million statements from 435,000 articles and 1,900 textbooks.
Formal theorem search: AViD does not compete with Mathlib semantic search engines; it consumes Leandex as infrastructure and adds a decision layer that issues novelty verdicts.Leandex searches Lean 4 declarations, while Lean Finder incorporates user intent into semantic Mathlib search.
Novelty filtering: Unlike LeanConjecturer, AViD’s contribution is composing existing exact-match and aesop filters with D3, an informal branch, temporal filtering, and external evaluation.LeanConjecturer generated 12,289 conjectures from 40 seed files, of which 3,776 were syntactically valid and non-trivial.
Proof similarity: AViD repurposes premise-set representations from premise selection and theorem-similarity research: D3 fingerprints finished proofs to assess redundancy rather than selecting premises to construct proofs.Before computing Jaccard distance, AViD removes ubiquitous Init. and Lean. premises so similarity reflects mathematical content.
Pipeline positioning: Existing paper-to-Lean pipelines verify correctness but not novelty, whereas AViD assembles search, formalization, and similarity infrastructure into a pipeline that maps LaTeX papers to verdicts.A Lean file may compile without errors yet fail to faithfully formalize the original statement.

3 The AViD Pipeline

The AViD Pipeline takes a LaTeX source file, formalizes its mathematical content in Lean 4, and uses a three-dimensional decision tree to produce a novelty verdict.

The system receives a .tex file as its input.
It extracts mathematical blocks from the source file for formalization.
It formalizes the extracted statements in Lean 4 and applies a three-dimensional decision tree to issue a novelty verdict.

3.1 LaTeX Ingestion and Parsing

The LaTeX parser identifies theorem-like environments, extracts their dependencies, and orders formalization topologically, while excluding non-formalizable environments from later stages. Its fixed environment vocabulary cannot parse some AMS-TEX or idiosyncratically named papers, making 7 of 33 withdrawn-dataset candidates non-viable.

Parsing capabilities: The parser recognizes standard, Spanish, abbreviated, and user-defined theorem-like environments in LaTeX.Supported forms include theorem, lemma, proposition, corollary, definition, their Spanish variants, abbreviations such as thm and prop, and environments declared with \newtheorem.
Dependency ordering: Cross-references and citations define dependencies, which are ordered with Kahn’s algorithm so independent blocks are formalized first.The parser builds a directed acyclic graph from \ref{} and \cite{} relationships, then processes dependent blocks afterward.
Formalization selection: Only theorem, lemma, proposition, corollary, and variants proceed to formalization; remarks, examples, proofs, and non-required definitions do not.These excluded environments may still be extracted, particularly when definitions are not needed as dependencies.
Known limitation: 7 of 33 withdrawn-dataset candidates proved non-viable because the fixed-name parser cannot handle some AMS-TEX or idiosyncratic environments.The limitation arises from compiled regular expressions and a fixed list of environment names, excluding examples such as amsppt, inizio, and numero.

3.2 Formalization in Lean 4

The pipeline delegates Lean 4 formalization to configurable language-model providers, using iterative compiler feedback and complexity-based modes. Papers share a versioned Lean project, while real-paper experiments use statement-only formalization, leaving proof-premise analysis unexercised.

3.2.1 Multi-model Abstraction: Formalization is delegated to a ModelProvider interface supporting eight backends, with experiments using Qwen 3.7-max through OpenCode Go.The selected backend was chosen by empirical comparison across providers.
3.2.1 Multi-model Abstraction: Agentic providers verify Lean code internally, whereas API providers rely on external compilation and iterative error feedback.The external cycle extracts code, compiles it with lake env lean, and resubmits errors for correction.
3.2.1 Multi-model Abstraction: Blocks are assigned SIMPLE, MEDIUM, HARD, or EXTERNAL modes according to estimated complexity and permitted correction rounds.The modes allow 5, 15, or 30 maximum correction rounds, while EXTERNAL emits an axiom with a source reference.
3.2.2 Shared Lean Project: All papers share Lean 4 version 4.29.0 with a Mathlib build containing 8,247 .olean files and an orchestrator-consulted theorem index.Each paper is hosted as a submodule, and formalized blocks accumulate in its Paper.lean file.
3.2.2 Shared Lean Project: The demanding full-formalization criterion requires error-free compilation, no sorry declarations, and at least one substantive declaration.Empty files and import-only files are rejected, but the criterion does not guarantee semantic fidelity.
3.2.3 Statement-only Mode: Statement-only mode accepts a compiled Lean statement containing := by sorry, configuring prompts and acceptance criteria rather than adding a native codebase capability.This mode relaxes acceptance to compilation without errors.
3.2.3 Statement-only Mode: All experiments on real papers use statement-only mode, so D3, which requires premises from a proof, is not exercised.This limitation affects the reported real-paper experiments specifically.

3.3 Reference Corpora

The system compares each statement against formal, informal, and paper-local reference corpora. Formal matches use Mathlib, informal candidates combine temporally complementary sources, and the local index prevents self-duplication within a paper.

Reference corpora: The system compares each statement against three corpora: formal, informal, and its own paper-local index.The local index is consulted before Mathlib to avoid labeling a theorem introduced earlier in the same paper as pre-existing.
Formal corpus: Mathlib v4.29.0 is accessed through Leandex, which indexes statements and returns matches with proof status.Because the API provides no similarity scores, the system uses result ordering and discards statement_only results.
Informal corpus: The informal corpus combines TheoremSearch’s 9.2 million statements with Matlas’s 8.07 million journal statements spanning publications since 1826.TheoremSearch covers arXiv and seven additional sources, while both services expose public APIs without authentication.
Informal corpus: Retrieved informal candidates are filtered using MiniLM embeddings with a cosine-similarity threshold ≥0.40 before subsequent filters and the LLM judge.This filtering stage precedes the filters described in section 3.4.1 and the final LLM assessment.

3.4 The Three Dimensions

The pipeline evaluates novelty along three dimensions: prior existence, automatic triviality, and structural distance between proofs. These dimensions use ordered corpus and tactic checks, plus a Jaccard-based proof comparison whose threshold remains uncalibrated.

D1: Prior existence: D1 checks prior existence in formal and informal corpora, short-circuiting the informal search when the formal corpus finds a match.The formal fallback uses exact? to find an existing theorem, while the informal branch queries TheoremSearch and Matlas and applies structural filters plus an LLM judge.
D2: Automatic triviality: D2 labels a statement trivial if any standard automatic tactic closes its Lean formalization within the configured tactic budgets.The tactics run in a fixed order, with 10 seconds for the first five and 30 seconds for aesop; the result depends on the formalized statement, tactic, and budget.
D3: Structural distance: D3 measures proof difference using Jaccard distance over deduplicated, filtered premise sets, treating proofs as structurally distinct when distance exceeds θ = 0.5.Empty post-filter premise sets yield an INCONCLUSIVE verdict, and θ = 0.5 is an initial design value not calibrated broadly.

3.5 Verdict Tree

The verdict tree evaluates triviality, formal-corpus matches, informal-corpus matches, and proof distance in increasing cost order. It emits novelty classifications, but three D3-dependent verdicts are unavailable in the statement-only experiments, while generalization or specialization cases require human review.

Evaluation order: D2 tests triviality first; if a standard T_AUTO tactic closes the theorem, the tree returns NOT_NOVEL_trivial without consulting external APIs.D2 is local and cheap, so it short-circuits the pipeline when the theorem is trivial.
Evaluation order: The tree then queries formal corpus C𝐹 before informal corpus C𝐼, with C𝐼 requiring several APIs and an LLM judge.D1 C𝐹 is a fast HTTP query, whereas D1 C𝐼 uses a temporal filter and LLM judge.
Experimental scope: Three verdicts—PROOF_NOVELTY, NOT_NOVEL_redundant, and INCONCLUSIVE—depend on D3 and are not emitted in the statement-only experiments.D3 runs only for a C𝐹 match requiring a proof-novelty decision, and it is the most expensive dimension because it extracts premise sets.
Verdict outcomes: The eight outcomes include STATEMENT_NOVELTY, PROOF_NOVELTY, KNOWN_IN_LITERATURE, NOT_NOVEL_redundant, NOT_NOVEL_trivial, GRAY_ZONE, MATCH_PENDING_D3, and INCONCLUSIVE.GRAY_ZONE covers judge classifications of generalization or specialization and requires human review.

3.6 Implementation and Current State

The system is implemented in Python 3.11+ as modular parser, novelty, and formalization orchestrators, with a verdict tree invariant to the formalization orchestrator. Its current state includes 153 passed tests, 1 skipped test, an evaluation set of 24 theorems, and 26 withdrawn papers with matched controls.

Implementation: The Python 3.11+ codebase separates parsing, novelty orchestration, and the three novelty dimensions from formalization orchestration with multi-model abstraction.The implementation is organized into two modules.
Implementation: The verdict tree remains identical regardless of which orchestrator formalized the paper.
Current State: 153 tests passed and 1 was skipped; the evaluation set contains 24 theorems and 26 papers withdrawn for duplication, with controls matched by category and year.

4 Instrument Validation

Instrument validation shows that D2 achieves strong performance on cases with defined expectations, while D3 and D1 expose important calibration and measurement limits. In particular, D3 measures distances between formalizations rather than underlying ideas, and D1’s apparent matches cannot establish coverage or precision with the current API and evaluation design.

D3 calibration: D3’s five-pair calibration supports θ=0.5 as a design choice, not a calibrated optimum, because only T08 and degenerate T07 constrain the admissible interval.T08 requires θ<0.7222, while T07 requires θ≥0.50; the evidence therefore supports θ<0.7222, with θ=0.5 selected within that range.
D3 limitations: D3 measures distance between formalizations, not informal mathematical ideas, because distinct strategies can converge to the same canonical Mathlib lemma.The relationship between formal proof distance and distance between underlying ideas remains unestablished; the authors report D3 relative to Mathlib v4.29.0.
D2 validation: D2 is sensitive to the concrete formal statement and tactic budget, with T23 avoiding a prior false positive and T14 succeeding where a more complex version exceeded the budget.These cases illustrate that tactic outcomes depend on the statement produced by the formalizer.
D2 validation: D2 succeeds on 22 of 24 evaluated theorems (91.7%); among the 22 cases with defined expectations, it records no false positives or false negatives.T19 and T22 remain in the denominator but lack binary expectations for success measurement.
D1 validation: D1’s C𝐹 branch found matches for all 18 non-trivial theorems reaching it, but this is not measured coverage because the criterion accepts the first Leandex result without a similarity threshold.The six unmatched cases were never queried because D2 detected them as trivial, and the current API provides no scores for filtering.
D1 validation: The C𝐼 branch was never activated because no theorem satisfied its entry condition: D2 negative and C𝐹 without a match.All non-trivial cases had a C𝐹 match, while cases without one were stopped earlier by D2.

5 Experiments

The evaluation on withdrawn arXiv articles identified three implementation-independent obstacles: compilation does not ensure semantic fidelity, retrieval recall is limited by index coverage, and withdrawal removes source needed for reproducible benchmarking. Operational findings also exposed retrieval defects and showed that statement-level similarity was not a useful duplication discriminator in this set.

Dataset construction: The benchmark yielded 26 viable withdrawn articles and 52 category- and year-matched controls from 382 examined candidates.The withdrawn articles spanned 17 categories and years 2001–2026; controls were not withdrawn and had verifiable sources.
Dataset limitations: ArXiv source removal undermined reproducibility: none of 25 sampled withdrawn duplication articles retained downloadable source.A LaTeX-first pipeline can process such articles only if their sources were downloaded before withdrawal.
Formalization fidelity: Seven of 10 articles were formalized, but compilation did not establish semantic fidelity because formalizations could omit equivalence directions or replace content with placeholders.Two failures exceeded the model limit, while auditing remained necessary because syntactic tests cannot decide whether generated Lean code means the original statement.
Pipeline defects: Excluding self-retrieval corrected three false non-novelty verdicts, while temporal filtering corrected matches to later works and exposed two generic index defects.With both corrections, one control match and no withdrawn-article matches were detected; the control match used an approximate formalization.
Retrieval coverage: A duplicator absent from the reachable corpus imposes a recall ceiling of zero, regardless of similarity metric, embedding threshold, or judge.Most identified duplicators predated arXiv, and broader searching confirmed that their absence reflected corpus coverage rather than method quality.
Detection results: Statement-level scores did not distinguish duplication in this set (p= 0.854).A control match was correct but irrelevant because it retrieved a similar attributed work rather than the duplicated result.

6 Conclusion

AViD Journal operationalizes automatic novelty verification from LaTeX formalization to a verdict, but does not solve the problem. Its evaluation identifies transferable infrastructure obstacles and shows that the main bottleneck is not metric design alone.

System and evaluation: AViD Journal traverses the path from a LaTeX article to a novelty verdict using Lean 4, three reference corpora, and an eight-verdict decision tree.The pipeline formalizes statements with abstraction over eight backends and evaluates its decision dimensions in increasing cost order.
System and evaluation: D2 succeeded on 22 of 24 theorems (91.7%), while D3 matched human judgment in five calibration pairs and D1 found matches in all 18 queries reaching that stage.The D1 matches lack a similarity threshold, so they do not distinguish genuine corpus coverage from unfiltered retrieval.
Structural obstacles: The evaluation identified three transferable obstacles: compilation does not ensure semantic fidelity, theorem-index coverage limits recall, and arXiv withdrawal removes sources needed for reproducible benchmarks.These obstacles are properties of the problem and available infrastructure rather than deficiencies of this implementation.
Remaining limitations: The framework measures novelty over separate statements and frozen proofs, missing novelty from combinations, definitions, transferable methods, and conceptual reformulations.Its Jaccard premise distance is an engineering approximation that can produce false positives and false negatives, while D3 currently applies only to Prop.
Conclusion and future work: AViD Journal does not solve automatic novelty verification; the work argues that answering whether it can be automated requires building the system, testing real ground truth, and reporting failures.Future work includes larger externally labeled evaluations, self-formalized arXiv benchmarks, improved calibration, and reduced dependence on individual formalizers.