stat.COOct 26, 2026
SaveKAPPA: Checking the Proofs in Statistics Papers with Lean 4 and Language Model Agents
Organizations: Department of Statistics, Purdue University, West Lafayette, IN 47907, USA
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.
Figures & tables
| Expert formalization | Language model prover | Language model review | This kit | |
|---|---|---|---|---|
| What is checked | the theorem, by any proof | a given formal statement, by any proof | the text of the paper | the paper’s statements, by the paper’s proofs |
| Who writes the formal statements | experts | people who set the problem | nobody | agents, reviewed by other agents before proving |
| Evidence | Lean kernel | Lean kernel | an informal opinion | Lean kernel and recorded reviews |
| When a proof fails | the expert repairs it | little information | a comment that needs checking | a located and classified issue, or the step where the check stopped |
| Cited results | formalized or assumed | not applicable | read | explicit hypotheses, listed for a person |
Table 1: Four ways of checking the proofs in a paper.
| Verdict | Requirements |
|---|---|
| Verified unconditionally | The statement passed the review before proving; the whole statement is proved along the paper’s route; the gated statement is unchanged; the build is clean, only the three standard axioms of Lean are used and no sorry is reachable; no external parameter or recorded debt remains; the final audit passed. |
| Verified conditionally | As above, but the proof takes explicit external parameters (a cited lemma, a fact the paper asserts without proof, a clause of another result), each listed with the step that uses it. |
| Issue recorded | A problem in this result’s own statement or proof, confirmed independently: by a reviewed Lean counterexample, or by a second agent’s review of the reasoning. The record names the side at fault (Table 3 ). |
| Unfinished | No conclusion yet, with the reason (for example, a missing library interface); not counted against the paper. |
Table 2: The four verdicts.
| Class | Meaning |
|---|---|
| The paper | |
| ERROR | The printed conclusion is false; a counterexample exists. |
| PAPER_ARGUMENT_GAP | The justification given for a step does not hold; the conclusion may still be true. |
| PAPER_ASSUMPTION_GAP | A step needs a hypothesis that the paper does not state and that cannot be derived. |
| EXPOSITION_GAP | The conclusion is true, but some range or case is not covered. |
| DOMAIN_CLARIFICATION | The objects are ambiguous, and the conclusion depends on the reading. |
Table 3: Issue classes.
| File | Contents |
|---|---|
| verification/RESULTS.json | The state of every result: stage, verdict, conditions, evidence paths. |
| verification/audits/ | Gate, final-audit, mechanical-check and issue reports, one per review. |
| pv_work/*.lean | Statement files, proofs, counterexamples; each compiles at the pinned versions. |
| verification/BLOCKERS.md | Recorded issues, with places in the paper and classes. |
| verification/report/ | The author report, a list of files to check, and a worksheet for the external inputs. |
Table 4: Main records of a project.
| Mechanism | Guarantee | Section |
|---|---|---|
| Statement review before proving; fingerprints | The statement proved has been compared with the paper, and it cannot change unnoticed | 5.2 |
| Proof along the paper’s route; failing steps kept as gaps | A verdict is about the paper’s argument, not about some other proof | 5.2 |
| Inputs as named hypotheses, with provenance | Nothing is assumed silently; a conditional verdict says what remains to check | 3 |
| Separate writers and reviewers; issues confirmed by a second agent, with a counterexample when possible | No result is passed, and no problem recorded, on one agent’s word | 5.1 |
| Mechanical audit and validator | The verdict agrees with its evidence: axioms, closure, hypotheses used, conditions | 5.3 , 5.4 |
| All state in files; offline replay | Every verdict can be rechecked without a language model | 5.4 , 8 |
Table 5: The mechanisms of the kit and what they guarantee.
Figure 1: The three stages of a check and the agents of each. Shaded boxes are reviews by agents other than the writer. The architect lists the results; every result then passes through drafter, gate, prover and auditor, with the issue checker called when a step of the paper is not justified; the compiler and the fact check produce the report.
| Role | Model | Writes |
|---|---|---|
| architect | Sonnet | inventory of results, dependencies, citations |
| drafter | Sonnet | Lean statement and step obligations |
| gate | Opus | review of the statement, before proving |
| prover | Sonnet, then Opus | the proof, along the paper’s route |
| auditor | Opus | final audit; counterexample and reasoning reviews |
| issue checker | Opus | ruling on a suspected issue; counterexamples |
Table 6: Roles. The coordinator runs on Sonnet.
Figure 2: The stages of one result. Shaded stages are reviews by agents other than the writer; the gate records fingerprints of the statement, which the final audit compares. A result whose predecessors are not yet proved uses their clauses as parameters and is reconnected later (not shown).
| Feature | Where it occurred |
|---|---|
| Verified unconditionally | E1 2.1, 2.2, 2.4; E2 2.1, 2.3, 2.5; E3 2.1, 2.4; E4 2.1; B 2.5, 4.12, 5.3; C 5.15 |
| Conditional on a cited result, (i) | E1 2.3; E4 2.2, 2.3; A 3.3 |
| Conditional on an asserted fact, (ii) | A 3.4; C 5.14 |
| Conditional on a clause of a result with an issue, (iv) | E3 2.3; B 3.3; C 5.17, 5.14, 2.2 |
| Conditional on a standard fact missing from the library, (v) | C 5.14, 2.2 |
| ERROR with a Lean counterexample | E1 2.5; E2 2.4; A 3.5; B 2.8, 4.8 |
Table 7: Where each verdict, class and mechanism occurred in the case studies (E1–E4: example papers; A–C: published cases; first round unless stated).
| No. | Answer key | Run | Score |
|---|---|---|---|
| 2.1 | unconditional | unconditional | agrees |
| 2.2 | unconditional; the expansion is a fair implicit step | unconditional; the expansion recorded as a fair implicit step | agrees |
| 2.3 | conditional on the cited inequality, (i) | conditional on Popoviciu’s inequality, (i) | agrees |
| 2.4 | exposition gap (case ), or unconditional with that case filled in | unconditional; the case ruled a fair implicit step and filled in | accepted |
| 2.5 | ERROR , with a counterexample | ERROR ; counterexample , | agrees |
| 2.6 | conditional on the clause of 2.5, (iv) | PAPER_ARGUMENT_GAP in its own proof, with 2.5’s issue upstream | differs |
Table 8: The first example paper: the answer key, written before the run, and the verdicts of the run. The run took 82 minutes and cost $14.54.
| No. | Answer key | Run | Score |
|---|---|---|---|
| 2.1 | unconditional | unconditional | agrees |
| 2.2 | DOMAIN_CLARIFICATION | DOMAIN_CLARIFICATION ; open reading proved, closed reading refuted | agrees |
| 2.3 | conditional on the asserted concavity, (ii) | unconditional; the concavity proved from Mathlib | differs |
| 2.4 | ERROR | ERROR ; counterexample , | agrees |
| 2.5 | unconditional, constant before | unconditional, constant before | agrees |
| 2.6 | PAPER_ASSUMPTION_GAP or PAPER_ARGUMENT_GAP | PAPER_ARGUMENT_GAP ; the first step refuted | agrees |
Table 9: The second example paper. The run took 75 minutes and cost $14.74.
| No. | Answer key | Run | Score |
|---|---|---|---|
| 2.1 | unconditional | unconditional | agrees |
| 2.2 | conditional on Glivenko–Cantelli, (v) or (ii); (i) acceptable | conditional on Glivenko–Cantelli, (i) | accepted |
| 2.3 | unfinished, TRANSLATION_BLOCKED ; conditional with the Brownian bridge as an explicit parameter acceptable | conditional on Donsker’s theorem and Kolmogorov’s formula, the Brownian bridge defined by its properties | accepted |
Table 10: The fourth example paper. The run took 81 minutes and cost $14.32.
| No. | Key | Run | Our check |
|---|---|---|---|
| 2.3 | verified | PAPER_ASSUMPTION_GAP : missing | correct, minor |
| 2.5 | verified | unconditional | — |
| 2.8 | verified | ERROR : fails when vanishes near | correct, minor |
| 3.1 | PAPER_ARGUMENT_GAP | PAPER_ARGUMENT_GAP in the induction step | the published error |
| 3.2 | verified | PAPER_ARGUMENT_GAP ( for signed ) and DOMAIN_CLARIFICATION | correct, minor |
| 3.3 | conditional, (iv) | conditional on the clause of 3.1 | — |
Table 11: Case B, version 2 on arXiv. “Key” is the answer key written from the corrigendum before the run; “our check” is the hand check of every finding that the key did not anticipate. The run took 171 minutes and cost $65.24.
| Paper (results) | Correctly classified | Faithful in Lean | Hidden or without Lean evidence |
|---|---|---|---|
| A (5) | 5 / 5 / 5 | 3 / 3 / 0 | 0 / 2 / 3 |
| B (12) | 12 / 9 / 10 | 10 / 5 / 0 | 0 / 4 / 8 |
| C (6) | 6 / 6 / 6 | 2 / 4 / 0 | 0 / 0 / 2 |
| Total (23) | 23 / 20 / 21 | 15 / 12 / 0 | 0 / 6 / 13 |
Table 12: The kit, the direct agent and the direct chat on the three published papers (entries kit / agent / chat). “Faithful in Lean ”: verdicts backed, without conditions, by a compiled, sorry -free theorem stating what the paper states. The kit’s other verdicts are conditional, with every input a named hypothesis of the theorem. “Hidden or without Lean evidence”: verdicts that rest on an input assumed without saying so, on a statement narrower than the paper’s presented as the paper’s, or on no Lean file at all.
| Earlier design | Version 1.3 | Change | |
|---|---|---|---|
| Cost (list price) | 65.04 | 13.68 | |
| Tokens processed (millions) | 73.2, 64.1 | 31.2, 21.9 | |
| Time, sum of sessions (minutes) | 84, 83 | 51, 30 | |
| Verdicts as in the answer key | 3/3, 3/3 | 3/3, 3/3 | |
| False alarms; unfinished | 0; 0 | 0; 0 |
Table 13: Two runs of the earlier design and two of version 1.3 on the three-result benchmark paper. Changes are between the means.
| Run | Major | Moderate | Minor | Total |
|---|---|---|---|---|
| Two-lemma example | 1 | 3 | 5 | 9 |
| Full-workflow example, first report | 1 | 7 | 6 | 14 |
| Full-workflow example, report after revision | 1 | 5 | 8 | 14 |
| Sample variance (E1) | 1 | 3 | 9 | 13 |
| Proportions and sums (E2) | 1 | 3 | 7 | 11 |
| Linear shrinkage (E3), first report | 1 | 5 | 10 | 16 |
Table 14: Problems found by the fact check in the first draft of each report.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
| Command | What it does |
|---|---|
| /pv-setup | checks the Lean environment, has the architect list every numbered result with its place in the paper, its dependencies and its citations, and writes the records |
| /pv-run | the coordinator’s loop: takes each result through draft, gate, proof and final audit, sends suspected problems to the issue checker, and records verdicts, until every result has one |
| /pv-resume | continues after an interruption: reconciles half-finished agent outputs with the records and resumes the loop |
| /pv-revise | handles a new version of the paper: compares it with the kept copy, resets only the affected results and marks their dependents for re-checking |
| /pv-report | writes the author report, the worksheet of external inputs and the index of files to check, and has them fact-checked |
| /pv-status | prints the progress table |
Table 15: Chat commands.
| Script | What it does |
|---|---|
| install.sh | creates a project, or upgrades one in place, keeping its records |
| scripts/pv_drive.sh | the unattended driver: short headless sessions, --auto-resume , --report |
| scripts/pv_lean.sh | compiles one file ( check ) or a module ( build ) with the pinned versions; refuses files with input-output actions |
| scripts/pv_status.py | all writes to the records ( record , add-tool , reset , human-check , set-deps ), the validator ( validate ), what can start now ( next ), what a revision changed ( defs-changed , followup ), and the progress table ( table ) |
| scripts/pv_audit_mech.py | the mechanical part of a final audit (Section 5.3 ) |
| scripts/pv_snapshot.py | saves and restores checkpoints of the records, and keeps the copy of the paper that revisions are compared with |
Table 16: Scripts.