Papers in statistical theory rest on long proofs that few readers check line by line. We present KAPPA (Kit of Agents for Proof-checking Papers with a proof Assistant), open-source software that organ...
PaperFormalizer is a Lean-based pipeline that assists authors in identifying and closing gaps in their research papers, converting them into Lean-verified versions. Starting from LaTeX, it transcribes the paper into a dependency graph, audits statements for faithfulness and correctness, and formalizes them in Lean using Mathlib and optional domain libraries. The process is author-in-the-loop, prompting the author whenever multiple interpretations exist and allowing them to accept, decline, or redirect proposed repairs, ultimately producing an annotated paper, a change report, and linked Lean code.
By Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet
SemantEq introduces a principled method for verifying that formal statements faithfully translate natural‑language mathematics by requiring each statement to transform into the other through a chain of allowed logical steps, rather than relying on trivial logical equivalence. The system evaluates proofs using Lean’s proof terms, achieving 100 % precision and 65.6 % recall on the ProofNetVerif test split, outperforming prior methods. A complementary audit tool, SemantEq‑ProofAudit, further improves recall for equivalent pairs while rejecting all non‑equivalent pairs.
By Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat, Rianna Jamdar, Yongxi Lin, Stella Biderman
The paper examines how AI‑written research papers often contain misattributed numerical claims. By re‑analyzing 540 judgments from a benchmark of nine AI agents on fifteen research problems, the authors manually labeled 256 claims and found that most failures stem from misalignment between the paper and the underlying work rather than outright cheating. They propose a deterministic claim‑to‑evidence checker that achieves over 90% precision and, when combined with an LLM verifier, offers a more reliable audit of AI‑generated research.
By Mosab Alfaqeeh, Omar Hourani, Muath Hourani, Hashem Alfaqeeh
arXiv:2610.17358v1 Announce Type: cross
Abstract: Formal verification proves that a program satisfies its specification, but says nothing about whether the specification captures what the author mean...
By Martin Amster, One An, Holly Baker, Fernanda Graciolli, Simon Henniger, Nada Amin
arXiv:2605.22875v2 Announce Type: replace
Abstract: Long-horizon mathematical reasoning fails less often because a model cannot produce a valid next step than because an agent fails to maintain and e...
By Zelin Zhao, Bo Yuan, Yuchen Zhu, Jaemoo Choi, Yongxin Chen