Cycle Consistency Pilot

Setup

The question: does giving a model access to the formal graph's dependency context improve autoformalization quality?

We measure this with a cycle-consistency test: take a real Lean 4 declaration F from Mathlib, have a model describe it in English (NL), then have a formalizer try to reconstruct Lean from NL alone. If the reconstruction F' matches the original F, the model preserved the meaning. The formal graph lets us provide F's dependencies — the declarations F actually uses — as context to the formalizer.

In a sentence: can knowing what a theorem depends on help you write it back in Lean?

The four conditions

We ran the formalizer (Claude Haiku 4.5 via Bedrock, same model for all) on the same 60 NLs under four conditions that vary only what context is appended:

Signature of a Lean declaration is the typed API — everything before the := (definition body) or by (tactic proof). For a theorem it's the statement itself; for a definition it's the type. It does not include the proof or the implementation. So the signature of ack_injective_left is (n : ℕ) : Function.Injective fun m => ack m n — enough to know how to invoke it, but not how it's proved. Throughout this page, "T provides dep signatures" means the formalizer sees the typed API of each predecessor, not its proof.

Predecessors of F are the nodes F directly depends on — the declarations whose names and types appear in F's signature or proof. They are the 1-hop outgoing neighbors of F in the formal graph (source_id = F, across all edge types: proof, sig, def, field, extends, docref).

Concrete example: what each condition actually sends

The candidate below is ack_inj_left from Mathlib.Computability.Ackermann — 7 predecessors, short signature, non-dense stratum. Toggle conditions to see exactly what the formalizer receives in each case.

How we scored each output

Type-check (primary): each output is wrapped in import Mathlib and run through lake env lean against Mathlib v4.29.0. Pass = elaborates without errors (sorry is allowed; it suppresses proof obligations but not type errors). This is model-free ground truth.

Judge (secondary): Claude Sonnet 4.5 is shown the target signature F and two candidate outputs with randomised A/B labels. It answers: which candidate more accurately matches the target semantically? The judge sees no condition labels and has no knowledge of which output came from which condition. Blinding map stored separately from results.

Edit distance: token-level Levenshtein between F's original signature and each output. Descriptive only.

Sample

60 Mathlib theorems and definitions (seed 42), stratified by in-degree (how widely cited: dense/medium/non-dense) × signature length (large/small). 10 per cell. All four conditions share the same 60 NLs — only the formalizer input varies.

1. Core Finding: Signatures Are the Load-Bearing Component

The type-check rate across all four conditions is the cleanest summary.

The marginal typecheck rates for B and T-names are identical (both 33%), but the paired picture is more interesting. T-names doesn't help the same candidates as B — it lifts some and drops others, net zero:

Only 13/20 B-passes overlap with T-names passes. T-names shifts which candidates typecheck — 7 that baseline would fail it passes, and 7 that baseline would pass it fails. A plausible mechanism: dep names push the formalizer toward specific declarations in the neighbourhood; when it guesses the wrong one the output is worse than no hint at all.

What reliably moves the needle is type signatures: T-random (55%) shows that any same-area signatures help, and the full predecessor graph (63%) adds another 8pp by providing signatures directly constraining F's own types.

2. Pilot: Baseline vs. Treatment

Before running the ablation we ran the core B vs T comparison on all 60 candidates. The judge (Sonnet 4.5) was shown the original signature and the two outputs — B and T — with A/B labels randomised per item. It chose which matched the target better.

The judge strongly prefers treatment outputs (82% of cases). The Wilcoxon test on the paired +1/−1/0 coding is significant (p ≈ 0), but n=60 is underpowered for subtle effects — read this as a strong directional signal.

Stratified by in-degree × signature size:

Treatment wins in every cell. The strongest cell is dense × large: 10/10/0 (T/tie/B) — the regime where F is both widely cited and has a complex signature, meaning its dep context is richest and there is the most structure to get right.

3. Ablation: What Is Actually Doing the Work?

Why we ran it

The B vs T result is strong, but the treatment context does two things at once: it gives the model the right type signatures (structural) and reveals the mathematical domain via the predecessor names (topical). We can't tell from B vs T alone which of these is load-bearing.

Three new conditions let us pull them apart:

• B vs T-names: if T-names ≈ B, domain hints alone don't help — signatures are what matters.
• T-random vs B: if T-random > B, any same-area signatures help, not just predecessor signatures specifically.
• T vs T-random: if T > T-random, the actual predecessor relationship adds signal beyond "same neighbourhood."

What the judge saw

For each of the 60 candidates the judge was shown the original signature F and two outputs with randomised A/B labels — in one run T vs T-names, in another T vs T-random. Same prompt as the pilot: "which candidate more accurately matches the target signature semantically?" B vs T-names and B vs T-random were not judged directly; those comparisons come from the typecheck rates (which are model-free and don't require transitivity).

What it tells us

The judge and the type-checker agree directionally but not in magnitude:

The judge and typecheck diverge most on T vs T-random (judge: 45/37 nearly tied; typecheck: 63% vs 55% with an 8pp gap). The next section shows why.

4. Why Judge and Type-Check Diverge on T-random

The judge evaluates whether an output statement is semantically plausible given the NL. The type-checker asks whether it elaborates — are the names, argument types, and return type actually well-typed in Lean?

A T-random output can look plausible — it uses the right vocabulary because same-module declarations share types and namespaces — but fail to elaborate because the specific argument structure is wrong. The judge rates it highly; the type-checker rejects it. These are different failure modes, not one metric being "wrong."

The scatter below maps each of the 60 candidates on two axes: did the judge prefer T or T-random? Did T type-check when T-random didn't (or vice versa)? The shaded top-right region contains candidates where the judge preferred T-random but T was the one that actually type-checked.

If the scatter is dense to read quickly, here's the same data as a 2×2 count table — judge verdict (rows) × whether T was the one that type-checked (columns):

5. Edit Distance to Target Signature

Token-level Levenshtein between F's original signature and each output. Smaller = closer to the ground truth structurally. This is a distance metric, not a validity metric — an output can be close in edit distance but still wrong, or far but semantically equivalent.

6. Per-Candidate Detail

7. Generalization: 5 Projects, 300 Candidates

The pilot and ablation in §1–§6 were Mathlib-only (n=60). To test whether the findings generalize, we replicated the entire protocol — same models, same prompts, same judge, same seed — on 4 additional Lean 4 projects downstream of Mathlib, spanning very different mathematical domains:

Each project contributed 60 uniformly-sampled candidates (unstratified — small projects can't fill the 3×2 in-degree × signature-size grid). Total: 300 pilot B-vs-T pairs and 300 ablation pairs. Per-project judge counts in the three tables below.

7.1 Headline (B vs T) replicates everywhere

7.2 Signatures finding (T vs T-names) replicates everywhere

7.3 Predecessor-vs-random (T vs T-random) does NOT replicate

7.4 What the five projects tell us

The three findings now have very different levels of empirical support:

The original Mathlib pilot's T-vs-T-random gap (+8pp, CI [−8.3, +25.0]pp) does not survive replication. Across four additional projects the gap centres on zero (−3, −3, 0, +2). What the formal-dependency graph actually buys you at this formalizer scale is the typed API of namespace-adjacent declarations — not the specific selection of predecessors.

This is a sharper result for the talk than "the graph helps". It says: a small, locally-typed context window helps the formalizer enormously, and the graph is a fine source of such a context — but if the goal is just "give the formalizer relevant typed API", you could draw from the same Lean module instead and get the same outcome. The interesting graph-specific claims live elsewhere (e.g. ranking, distant retrieval, multi-step proof assistance) and would require different experiments.

What this scaled study still doesn't cover:

• Typecheck signal: skipped for non-Mathlib because each project pins its own Lean toolchain. The Mathlib typecheck (§1) is the only "model-free validity" pass.
• Stratified breakdown: only Mathlib has enough density to fill the in-degree × signature-size grid.
• Larger n per project: 60 is enough to detect 30pp gaps, but tying down small gaps (e.g. testing if T-random truly equals T) would need n ≈ 300+.

8. Limitations

• n = 60. Pairwise 95% CIs on typecheck-rate differences are ~±13–16pp. The B = T-names result (0pp gap) is the most robust claim. The T vs T-random gap (8pp) is directional only.

• T-random is a weak null. Same-module nodes share vocabulary and types with F. On average 38% of a candidate's predecessor names share its top-level namespace prefix; 17/60 candidates have >50%. A stronger null would be random nodes from a different module entirely.

• Typecheck and judge measure different things. Typecheck = elaborability. Judge = semantic plausibility of the statement. Both matter; neither supersedes.

• No Opus judge. Sonnet 4.5 judges Haiku 4.5 outputs; both have Mathlib in their training data. B vs T-names and B vs T-random were not judged directly — LLM judge preferences are not reliably transitive.

• Namespace leakage. The verbatim-name check in validation passes, but predecessor names implicitly identify F's mathematical area (38% mean same-namespace dep overlap, 17/60 candidates >50%). This is a confound for any claim about topical vs. structural signal.

• NL name leakage. The informalizer was not told to avoid mentioning F's name. Post-hoc: 10/60 NLs contain F's last name component verbatim; 9/60 contain a CamelCase part. Sensitivity check on the clean-NL subset (46/60): B = 32.6%, T = 63.0% — identical to the full sample (33% / 63%), so the finding is robust but gap magnitudes are conservative-biased toward zero when the name is present in both prompts.

• Dep context truncation in dense-large stratum. The 8 000-token cap (≈32 000 chars) truncated deps for 2/10 dense-large candidates (up to 29 deps dropped). For those candidates, T's context is the first ~150 deps by edge-type + name order, not all deps. The `dep_truncated` column records exact counts.

• F_T uses F's exact name 21/60 times vs F_B 8/60. The judge sees the correct declaration name in T's output more often, which may inflate judge preference for T independent of semantic quality. This is one more reason to treat typecheck rate as the primary metric.