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 s=0 ), or unconditional with that case filled in
unconditional; the case s=0 ruled a fair implicit step and filled in
accepted
2.5
ERROR , with a counterexample
ERROR ; counterexample n=2 , x=(1,−1)
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 n=1 , p=1/10
agrees
2.5
unconditional, constant before n
unconditional, constant before n
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 : FX(0)=0 missing
correct, minor
2.5
verified
unconditional
—
2.8
verified
ERROR : fails when h vanishes near 0
correct, minor
3.1
PAPER_ARGUMENT_GAP
PAPER_ARGUMENT_GAP in the induction step
the published error
3.2
verified
PAPER_ARGUMENT_GAP ( X for signed X ) 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)
71.15,65.04
17.73,13.68
−77%
Tokens processed (millions)
73.2, 64.1
31.2, 21.9
−61%
Time, sum of sessions (minutes)
84, 83
51, 30
−51%
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
Appendix
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
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions. We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version. Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit. Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed. The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims. The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes. The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code. By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust. PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer. Papers with Lean code shared by users are available at https://paperformalizer.org.
Formal proofs in Lean 4 that pass the kernel's type checker can nonetheless vary widely in quality. We introduce ProofJudge, an agentic LLM-as-judge system that scores formal proof quality along five dimensions beyond correctness: library leverage, automation fit, structural clarity, statement quality, and Mathlib conventions. We evaluate ProofJudge on a novel dataset of 218 declarations drawn from distinct Mathlib PRs. The judge agent is grounded by tool access to the commit the PR is applied to, enabling it to query the library state when scoring. A judge is considered aligned with human preferences when it rates the version of the PR Mathlib accepted above the initial version that was sent back for revision. All six judge models evaluated recover the reviewers' preference well above chance, from 80.8% to 63.5%, and two open-weight judges reach roughly 70% at a tenth of the best judge's cost. We release the judge harness, evaluation dataset, and evaluation traces as open-source artifacts to support further research.
Verified proof edits offer a natural source of supervision for improving language-model-generated Lean proofs. Yet verification establishes that an edit is correct, not that its training signal is free of search artifacts. We introduce LeanPolish, a symbolic Lean 4 pipeline that releases 33,402 accepted local edits and 65,596 same-state failed attempts, and use it to study what models learn from this supervision. First-success search admits a goal-independent rule with perfect ranking accuracy; teacher-selected evaluation sites also reward trivial deletions. Continuing menu evaluation beyond the first success removes the ordering shortcut: a trained ranker selects the best candidate on 70.1% of evaluated held-out states, versus 36.9% for the strongest frozen baseline. For compression, iterating the symbolic pass raises miniF2F savings from 19.7% to 27.5%, exceeding the neural hybrids we test there. Verified neural editing helps on other proof sources, but matched frozen-model controls show that its gains need not come from training. The supervision does improve whole-proof rewriting: fine-tuning raises verified token reduction from 2.8% to 5.5% on 19 PutnamBench proofs. Together, the released edits, complete candidate pools, and controlled evaluations separate learning to imitate a search policy from improving on that search. They provide a reproducible basis for studying proof improvement while keeping correctness, compression, and edit policy distinct.