> ./projects --select "AVID Journal"
Automated Verification & Integrity Pipeline
Project Overview
AVID Journal is an automated framework designed to assist in the peer-review process of mathematical literature. It represents a novel approach to "Auto-formalization", aiming to bridge the gap between structured LaTeX documents and formal verification systems.
While LLM "Hallucinations" regarding strict syntax are a known hurdle (addressed in my separate reverse-translation experiments), this project confronts the Verification of Novelty: the difficulty of cross-referencing a new theorem against the immense, unformalized corpus of mathematical history to determine if it has been proven before.
> ./view --pipeline
- 1. Ingestion Raw .tex file processing and metadata extraction.
- 2. Structural Parsing Semantic segmentation. Identifying Boundaries of Definitions, Theorems, Lemmas, and Proofs. Currently utilizing Gemini, though rule-based heuristic parsing is being explored for improvement and determinism.
- 3. Formal Translation Neural-driven mapping. Gemini 2.0 is employed to translate natural language math into Coq code (selected for higher compilation success rates compared to Lean 4 regarding this specific task).
- 4. Formal Verification The generated code is passed to the Rocq (Coq) prover. If the proof checks, the theorem is marked as "Verified".
- 5. Novelty Evaluation Currently conceptual. While automated comparison against libraries like Mathlib is the long-term goal, the system currently acts as a force multiplier for human reviewers. By automating the logical verification (Steps 1-4), AVID allows referees to focus their expertise exclusively on judging historical novelty and context.
- 6. Publication Generation of verification metrics and formal validation reports for human reviewers.