The kernel of the Lean proof assistant checks that a proof establishes its statement. Whether the statement says what was intended is left to human reviewers. This is the old problem of validating a specification, and it grows more pressing as language models write formal statements in bulk and agents edit formal developments continuously. We present ProofPatch, a tool that helps reviewers judge Lean statements and keeps their judgments valid while the development changes. A reviewer can ask the kernel targeted questions about a statement, such as whether a hypothesis is needed or whether a counterexample exists. Each decision is stored with fingerprints of the statement as Lean elaborated it and of the definitions it depends on, and any declaration can be pinned so that a patch changing it is blocked, whether a person or an agent built on a large language model (LLM) wrote the patch. Working on elaborated terms rather than source text is the central design choice: notation and formatting changes leave a decision intact, and a changed definition reaches every theorem that uses it. On 229 pairs of consecutive revisions of Mathlib, Lean's mathematics library, ProofPatch sends 118 of 12,898 synthetic decisions back for review. Every text-based alternative misses at least 38 of these or sends back at least 13 times as many. On 1,527 labeled statements, kernel evidence flags unfaithful ones with precision 0.88 to 0.96, and in 344 runs of an LLM agent no change to a pinned statement got through.
Figures & tables
Figure 1: One review in ProofPatch. The reviewer acts on the artifacts in the middle row. Every fact in them comes from the kernel and from elaborated terms, not from text or from a model.
declaration, proof elided
receipts
lock
after patch
def clamp (lo hi x : Z ) : Z :=
definition
✗ lock fails
max lo (min hi x)
theorem clamp_le_hi (lo hi x : Z ) (h : lo ≤ hi) :
✓ alice
statement
re-review
clamp lo hi x ≤ hi
theorem lo_le_clamp (lo hi x : Z ) (h : lo ≤ hi) :
✗ alice
re-review
lo ≤ clamp lo hi x
Figure 2: The running example with its review state, and the gate’s verdict on a patch that rewrites the body of clamp as min hi (max lo x) . Shaded: clamp and the declarations whose statements depend on it. There are seven receipts on six theorems, five statement locks and one definition lock.
Figure 3: The evidence of one challenge as the reviewer sees it, from a real run that took 0.4 s. The hypothesis is needed, because subtraction on N truncates at zero. The last two rows are what a reviewer can rely on without reading the rest.
Method
sent back
needless
missed
statement diff
94
54
78
file diff
12,898
12,780
0
text closure
308
237
47
text closure with context
1,831
1,714
1
text closure on the kernel’s graph
290
210
38
text closure with context on the kernel’s graph
1,612
1,495
1
Table 1: Receipts sent back for re-review over the 229 revision pairs, out of 12,898. Needless: the elaborated statement and its dependency closure are unchanged up to definitional equality. Missed: the closure changed, but the method keeps the receipt.
Flagger
ProofNetVerif
graduate
synthetic
recall
acc.
strict evidence
0.953 (43)
1.000 (1)
1.000 (3)
0.049
0.424
broad evidence
0.928 (69)
0.875 (8)
0.500 (8)
0.081
0.439
LLM judge
0.905 (799)
0.513 (78)
1.000 (29)
0.872
0.845
judge with strict veto
0.903 (806)
0.513 (78)
1.000 (29)
0.878
0.847
Table 2: Flagging unfaithful statements. Precision per source, with the number of statements flagged in parentheses, and recall and accuracy (acc.) over all statements. The judge rows cover the 1,487 statements with a parsable verdict.
Figure 4: Kernel evidence beside the LLM judge. Left: precision per source, with the number of statements flagged. Right: on the flagged statements with a parsable judge verdict, whether the judge agrees and, if not, which side the label takes.
single round / with feedback
Tasks
n
accepted
declined
kernel error
caught
repair, examples
41
34 / 37
1 / 0
6 / 4
0 / 0
repair, Mathlib
31
4 / 7
0 / 6
27 / 18
0 / 0
adversarial, default prompt
50
5 / 6
41 / 37
4 / 2
0 / 5
adversarial, second prompt
50
6 / 6
9 / 16
31 / 24
4 / 4
Table 3: Agent runs with Qwen3.5-122B, each task once in a single round and once over up to three rounds with feedback from the gate. Declined: the model returned the file unchanged. Kernel error: the returned file did not compile. Caught: the gate refused a changed locked statement or a sorry .
Appendix figures & tables8 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 5: Components of ProofPatch. All clients run the same functions, and only the kernel service runs Lean. A challenge runs in a branch from the state before its target. An agent’s patch reaches the reviewer’s files only through the gate.
Figure 6: Statement screen for clamp_le_hi . Left: the informal statement above the formal one, split into its parts. Right: the evidence of the challenge that drops h , ending with the grade’s fixed wording, and alice’s receipt, which cites it. Bottom: the form that records a decision.
Figure 7: Dropping a hypothesis from three other theorems of the example: replay passes ( lo_le_clamp ), refuted with a kernel-checked negation ( vacuous ), and an alternative proof ( strict_of_le ).
Figure 8: Locks of the example project with their baseline fingerprints.
Figure 9: Gate report on the patch that rewrites clamp : the source diff, the effect on every declaration, the lock results, and the six receipts sent back for re-review.
Patch
Reported effect
Locks
Receipts
Verdict
body of clamp becomes min hi (max lo x)
body changed, six closures changed
5 of 6
1 of 7
blocked
body of clamp becomes if lo ≤ min hi x then min hi x else lo
definitional rewrite
6 of 6
7 of 7
accepted
bound variables of clamp become a b y
no change
6 of 6
7 of 7
accepted
clamp_of_mem becomes clamp_eq_self
renamed
6 of 6
7 of 7
accepted
proof of score_le_hundred becomes sorry
sorryAx added
6 of 6
7 of 7
blocked
statement of score_le_hundred becomes score x ≤ 101
statement changed
5 of 6
6 of 7
blocked
Appendix
Table 4: The gate on six patches to the running example, each applied alone and checked from the command line against HEAD . The file holds six locks and seven receipts. The columns count the locks that hold and the receipts that are kept.
Figure 11: One adversarial task of the evaluation, run with Qwen3.5-122B. The task cannot be solved as posed. The third answer changes what was asked, and the gate refuses it.
first elaboration of a Mathlib file, imports loaded once
458
13.5 s
43.3 s
reload after an edit to the last declaration
1
0.10 s
gate comparison, both revisions indexed
229
10 ms
34 ms
agent task, up to three rounds with the gate
244
26.8 s
116.8 s
Appendix
Table 5: Latency on the evaluation cluster, which has network storage and shared CPUs, as the median and the 90th percentile (p90). Interactive challenges and the reload, measured once, ran on the example project, probes on the labeled statements, and gates on Mathlib files.