Software checks statistical paper proofs step by step with lean
KAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
Artificial IntelligenceLogic in Computer Science
Summary
Checking long mathematical proofs in statistics papers is hard and often skipped by readers. The authors introduce KAPPA, a tool that uses AI language models and a proof assistant called Lean 4 to verify each step of these proofs against the original paper. KAPPA reports clearly whether each result is fully verified, conditionally verified, has issues, or is unfinished, helping find errors that were missed before. The tool works automatically, revisits only changes, and provides trustworthy evidence without relying solely on AI guesses.
What this means in practice
- •For statistical software developers: Automatically verify each step in statistical proofs within research papers to detect errors before publication or use.
- •For machine learning engineers: Use detailed proof verification in mathematical papers to ensure the correctness of theoretical foundations for AI models.
Authors
Zihua She, Xiao Wang
Abstract
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 organizes language model agents, run by Claude Code, to translate the proofs of a LaTeX paper into the proof assistant Lean 4 with its library Mathlib and check them there, result by result. Each numbered result receives one of four verdicts: verified unconditionally; verified conditionally, with every cited or unproved input stated as a named hypothesis; issue recorded, with its place in the paper and the side at fault; or unfinished, with the reason. The kit follows the paper's own proof step by step, rather than finding a new one. Separate agents write and review, each statement is compared with the paper before it is proved and fingerprinted afterwards, and every verdict rests on evidence that can be rerun without a language model. The kit runs unattended for hours, waits out usage limits, re-checks only what a revision changed and reports its cost by role, model and result. We describe the design, walk through a complete run, and apply the kit to four example papers with answer keys and to three published statistical papers, checked blind in their versions from before public corrections. In all three, the kit found the published error at the step that the correction names, together with further problems that we confirmed by hand. Given the same papers directly, the same language model working with Lean classified fewer results correctly on the longest paper and reported some statements narrower than the paper's as proved; no verdict of the kit claimed more than its Lean evidence showed.