Residual progress

The reported failure

Google DeepMind’s AlphaProof Nexus paper (arXiv:2605.22763) rates candidate proof sketches with a language model, because formal verification gives a binary signal and evolutionary search needs a graded one. Its raters judge, among other things, “the plausibility of remaining goals”. Its failure analysis reports:

the agent frequently offloaded a problem’s core difficulty into a single sorry within a helper lemma that reiterated the target statement in a slightly different form

and, of that behaviour:

Explicitly prompting against this behavior failed to prevent it.

Prompting is the wrong instrument. Whether a helper lemma reiterates its target is a relation between two propositions, and a proof assistant can sometimes settle it outright.

Where the instrument came from

This repository is a formalisation programme over eight open Erdős problems, and its output is structural: an exact carry normal form equivalent to irrationality for #68, a complete measure classification of the Mersenne achievement set for #257, the exact rank 2^e + 1 and an explicit odd-core basis of the dyadic totient kernel for #249, a first integral of the complex Newton flow for #1041, exact prefix-LCM dynamics for #269, and proved no-go theorems that close named strategies rather than gesture at difficulty. RESULTS states each result and the exact point where it stops.

Holding that line requires deciding, repeatedly, which of a programme’s many reformulations are progress. The instrument described here was built for that job, and it was turned inward first.

ErdosProblems/DemandLedger/Hyp.lean provides hypOf%, a term elaborator that takes the type of a named hypothesis binder directly from the kernel’s ConstantInfo and returns it as a standalone Prop. It does not pretty-print and reparse: the extracted proposition is the binder type or elaboration fails. An unresolved mathematical demand, which previously existed only in binder position, becomes an object that can be named, compared and proved about.

Applied to the 259 conditional-implication declarations in this corpus, it yields 101 distinct closed Props, of which 23 are substantial statements rather than side conditions. The finding, recorded in docs/semantic/zones/Z18.json, is blunt:

Fourteen of the substantial open antecedents of #249 — the pointwise, ray, multiple, diagonal, cone, jump, window, survivor, rank-two, cone-nonflat, prime-jump and nonintegrality supplies — are mutually implied, and the class is equivalent to Erdős #249 itself. … These are therefore not antecedents of the problem in any useful sense; they are the problem restated.

That is not a stylistic judgement about the reformulations. It is a proved mutual-implication class, and the reverse direction rests on a corpus completeness theorem. Fourteen apparent reductions of an open problem were, under the kernel, the open problem.

Basic.lean names those 101 demands and nothing more; the relations between them were proved once, by hand, for this corpus. The evaluator below is that audit turned into an instrument: the same question — does this remaining obligation differ from the target — asked per sketch, on demand, against a bounded proof budget.

Restatement is also a population effect

The fourteen are one class inside one problem. The wider question — whether a reformulation that restates its target is systematically less useful than one that does not — needs a corpus deep enough for the same problem to have been reformulated hundreds of times.

docs/reformulation_productivity.json records what this one has: 3,693 authored theorem-like declarations over two problems, roughly 1,846 each, against 3.7 Lean statements per Erdős problem in Formal Conjectures — a density ratio of 499. Generated certificate shards are excluded from the count; they are emitted in bulk and would swamp it.

Over the 654 measured statement nodes, split by whether a node restates its open problem:

Restatements are cited less and die more often. The file states its own proxy limits, and they are real: later reuse inside one corpus is not mathematical importance, and the author chose which routes to pursue, so this is a correlation over an unbalanced sample rather than a controlled comparison. It is offered as the measurement that exists, not as the one that would settle the question.

What the evaluator decides

scripts/residual_evaluator.py asks Lean three bounded questions about a sketch that targets P and leaves residual obligations R₁ … Rₙ:

1. Sufficiency. Is R₁ ∧ … ∧ Rₙ → P provable within the budget?
2. Restatement. For each Rᵢ separately, are both P → Rᵢ and Rᵢ → P provable?
3. Refutation. Is the residual demand provably false?

Four outcomes follow, and only two are vetoes:

Two details matter more than they look.

Restatement is tested per residual and in both directions. Testing P → ⋀Rᵢ instead is wrong: a target implies every legitimate consequence, so that criterion convicts every correct decomposition. An earlier version of this evaluator did exactly that and flagged a textbook base-plus-step induction split as the failure it is the opposite of.

A false accusation is the expensive error. Requiring two kernel proofs on one residual means a well-disguised restatement can escape into unknown_relation. That is the intended trade: missing one costs a wasted search branch, while falsely rejecting a productive change of representation costs the branch that would have worked.

ResidualBench

residualbench/ResidualBench.lean holds eight labelled sketches over two elementary targets — the sum of the first n odd numbers, and a divisor-count identity — including deliberate restatement, self-assumption, false-residual and hallucinated-literature specimens, plus two controls that must not be vetoed. Labels live in scripts/residualbench_manifest.json and are compared against the run; the evaluator refuses a manifest that tries to author a verdict rather than declare an expectation.

Under budget ladder_v3_independent:

Three vetoes, both controls clean, and the legitimate decomposition survives. docs/residualbench_report.json is the run: every proposition put to Lean, the tactic that discharged it, and its axiom budget. The same eight verdicts came back under this repository’s Mathlib and under the older one Formal Conjectures pins, so what the budget can and cannot reach is not an artefact of one library version.

Two rows disagree with their labels on budget grounds and are left that way. B_reassociation is an equivalent range reindexing and F_strengthening specialises a general arithmetic-progression formula; the current general tactic ladder does not close either. Adding tactics shaped to these fixtures would turn the benchmark into a transcript of its own tactic list.

D_self_assumption is an error by the author of the bench, kept on the record. Its residual is OddSum → OddSum, which is a tautology — equivalent to True, not to the target, because it cannot imply the target back. It was labelled endpoint_equivalent. The evaluator was right and the label was wrong. A residual provable with no assumptions establishes nothing and deserves its own verdict; it does not yet have one.

Running it

Requires a built Mathlib for this toolchain.

lake build ResidualBench
python3 scripts/residual_evaluator.py \
  --manifest scripts/residualbench_manifest.json \
  --lean-root . \
  --no-cross

The run emits, per sketch, the propositions it put to Lean, which tactic discharged each, and the axiom budget of every accepted proof. A tactic attempt counts as proved only when #print axioms returns a report free of sorryAx; a failed theorem still enters the environment closed by sorryAx, so the presence of a report is not sufficient. Each run carries two controls — one trivially provable proposition and one unprovable one — and refuses to report any verdict if the harness cannot separate them.

What this does not establish

The evaluator is sound where it speaks and silent elsewhere. It is not a proof-difficulty metric: logical strength and proof cost are different quantities, and a stronger residual may be easier because it has more exploitable structure. It is not complete: unknown_relation means the budget proved nothing, never that no relation exists. It has not been run against a live proof-search loop, so no claim is made here about search efficiency or solve rate. And no priority is claimed for the construction; the relation between this and existing proof-progress prediction and reward-model work has not been surveyed.

What it does establish is narrower and checkable: for the specimens listed above, at the stated budget, in the stated environment, the relation between a sketch’s remaining obligations and its target was decided by the kernel rather than estimated.