Beyond Correctness: Toward Automated Novelty Verification with Lean 4

• URL: http://arxiv.org/abs/2608.14669v1
• Date: Sun, 02 Aug 2026 18:49:03 GMT
• Title: Beyond Correctness: Toward Automated Novelty Verification with Lean 4
• Abstract summary: This article presents a pipeline that receives an article, formalizes its statements in Lean 4, and issues a novelty verdict through a decision tree over three dimensions.<n> Evaluation on papers withdrawn from arXiv due to declared duplication produced a result more informative than any performance measure.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• AI-Assisted Discovery and Construction of a Counterexample to the Convergence of Three-Block ADMM with the Identity Matrix as its Third Constraint Block [7.333795130390353]
  We show that direct three-block ADMM may fail to converge even when the first two blocks are strongly convex quadratics.<n>We also guide a study of multiplier relaxation and clarify when convergence can be restored at the fixed-instance and class levels.
  arXiv  Detail & Related papers  (2026-08-14T15:36:32Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game [0.0]
  We formalize a research result in the Lean 4 proof assistant by having a mathematician direct an AI system, and frame the activity as a formalization game.<n>The objective is to turn a document into Lean. The game is won when the development compiles, contains no sorry, and a machine check shows the target theorems rest on Lean's foundational axioms alone.<n>The case study is a complete, axiom-clean formalization of well-posedness for the nonlinear Vlasov equation via Dobrushin's mean-field route.
  arXiv  Detail & Related papers  (2026-07-09T23:17:54Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• Convergence Theory for Iterative LLM-Based Neural Architecture Search: A Parametric Cross-Entropy Framework with Closed-Form Proxy Reliability [48.83701310501069]
  Large language models (LLMs) are increasingly used as generators in iterative neural architecture search (NAS)<n>We model iterative LLM-NAS as a parametric Cross-Entropy (CE) method over executable programs.<n>We prove six results: (1) iterative LLM fine-tuning on elite architectures is equivalent to the CE update restricted to the LLM family; (2) expected architecture quality is monotonically non-decreasing across cycles; and (3) elite-set probability converges to a fixed point at a geometric rate.
  arXiv  Detail & Related papers  (2026-05-28T15:45:19Z)
• Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof [0.0]
  We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime.<n>We present three composable methods that together raise a skill from declared or tested to formal.<n>All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework.
  arXiv  Detail & Related papers  (2026-05-09T19:27:38Z)
• Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game [0.0]
  This paper identifies Architectural Reasoning as the necessary ability for future automated theorem discovery AI.<n>By renaming identifiers in the Natural Number Game in Lean 4, we created a zero-knowledge, closed environment.<n>We evaluate state-of-the-art models, finding a universal latency tax where obfuscation increases inference time.
  arXiv  Detail & Related papers  (2026-05-01T14:03:05Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• What Papers Don't Tell You: Recovering Tacit Knowledge for Automated Paper Reproduction [57.86097956633207]
  method is a graph-based agent framework for generating executable code from academic papers.<n>On an extended ReproduceBench spanning 3 domains, 10 tasks, and 40 recent papers, method achieves an average performance gap of 10.04% against official implementations.
  arXiv  Detail & Related papers  (2026-03-02T12:33:31Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  Logical reasoning is an important task for artificial intelligence with potential impacts on science, mathematics, and society. In this work, we reformulating such tasks as modular neurosymbolic programming, which we call LINC. We observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate.
  arXiv  Detail & Related papers  (2023-10-23T17:58:40Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.