Paper recorded by Signals 4 on 2026-10-14 in cs.AI. Abstract reproduced from arXiv; link to the original below.
Published 2026-10-14 on arXiv · recorded by Signals 4 on 2026-10-15
Category: cs.AI · 人工智能 · first seen 2026-10-15
We introduce a novel method for verifying Lean formalizations that goes beyond LLM-judged faithfulness. Unlike most verification methods, which rely on LLMs or trained models, our method combines LLM-based semantic review with mechanical numerical and vacuity checks, providing checkable feedback and detecting errors missed by LLM judges. We apply this method, along with our Extract-Verify-Proof au