Tested blindly on three articles before their official corrections, the open source tool located each error at the very stage designated by the erratum, and found others.
Theoretical statistics articles rely on long proofs that few readers check line by line. KAPPA, an open source software presented on arXiv, entrusts this work to language model agents piloted by Claude Code: they translate the proofs of a LaTeX article into the Lean 4 proof wizard, with its Mathlib library, and check them result by result, following the article's proof rather than looking for a new one.
Four verdicts, all replayable
Each numbered result receives one of four verdicts: unconditionally verified; conditionally verified, with each borrowed or unproven hypothesis named; problem noted, with its location and the offending part; or unfinished, with reason. Separate agents write and proofread, each statement is confronted with the article before being proven, and all conclusions can be double-checked without a language model. The tool runs on its own for hours, waits for the usage limits to be lifted, and only double-checks what a revision has changed.
Out of three published papers, reviewed in their pre-correction version, KAPPA found the error at the step cited by the erratum, plus other hand-confirmed issues. For comparison, the same model used directly with Lean ranked results on the longest paper worse and sometimes declared narrower statements than those in the paper to be proven, while none of KAPPA's verdicts exceeded what Lean had actually established.
Read the full article on the original source
Go to the source →