Preprint
Aug 2026
Beyond Correctness: Toward Automated Novelty Verification with Lean 4
AViD Journal is presented, 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 and an informal one, non-triviality via automatic tactics, and structural distance between proofs measured as Jaccard distance over premise sets.
A. Porto
· 0 citations