Proofs, claims, and oversight

Formal verification answers a precise question. A Lean proof that compiles establishes a theorem under stated assumptions. It does not automatically establish that the theorem is non-vacuous, that it matches the intended scope, or that the natural-language claim attached to it follows.

That gap is a useful place to study oversight because both sides can be made concrete: the machine-verifiable artifact signal is real, and claim-support labels in the restricted task can be backed by checked witnesses.

Proofs are the contact patch, not the terminal objective. They provide an experimentally privileged starting point: the verifier gives us an exact, inspectable artifact-validity signal, making the difference between satisfying a check and earning an inference unusually measurable.

That ground truth is bounded. Lean determines whether a proof establishes its formal theorem; it does not determine whether that theorem licenses the attached claim. Compilation fixes artifact validity before claim characterization. Selection then optimizes certificates against a separate bounded claim audit. Primary claim-fidelity labels come from checked witnesses in the restricted certificate task; natural-language transfer is optional and secondary.

A legitimate PASS can lend credibility to a claim or decision the checker never evaluated. The broader research target is that transfer of trust—and the auxiliary oversight signal required to keep it warranted under optimization pressure.

Central question: When claim certificates are selected for a useful but incomplete audit score, does selection reduce full witnessed fidelity or enrich unsupported authorizations relative to expected random selection from the identical pool—and does a selection-blind auditor still detect them?

Why this matters

This project grew out of model-assisted research. LLMs made symbolic production tractable at a scale I could not otherwise attempt, but they did not make the resulting conclusions trustworthy. As production became cheaper, determining what an artifact licensed me to believe, publish, or act on became the bottleneck.

Verifier optimization sharpens that problem: it can increase production of checker-approved artifacts without necessarily improving the claims attached to them. The experiment tests which additional oversight signal preserves that binding.

What exists now

Claim Fidelity is the checked prototype behind this work. It contains a pinned Lean 4 project, versioned claim schemas, positive and refusal fixtures, and a one-command verification gate.

• 32 Lean files and 99 unique theorem declarations after generated bundle re-inlines are excluded.
• No project-authored sorry tokens or explicit axiom declarations.
• A 60-second claim-gap demo passes the machine check and refuses an overreaching consequence at the claim layer, returning seven specific findings.
• A worked protocol unit binds four typed claims to Lean-checked witnesses, runs a configured structural linter, validates and scores exhaustive certificates, computes same-prefix selection contrasts, and isolates a selection-blind auditor interface. Its fixtures are hand-authored; it is not a model-behavior result.
• The exact public release is frozen as v0.2.0. A clean hosted run passed the compiled-environment recheck and complete nine-part gate.

This is prior apparatus, not evidence that the proposed model-behavior effect exists. Its job is to demonstrate the claim discipline and the ability to ship a reproducible formal artifact.

Where this extends nearby work

Recent work already establishes that compilation and semantic faithfulness diverge (FormalAlign, roundtrip verification, Beyond Compilation). Do LLMs Game Formalization? found no systematic gaming under its tested generation conditions, while LLMs Gaming Verifiers found that RLVR can favor shortcut strategies under extensional verification. This project asks a distinct causal question: whether increasing selection for a score from an incomplete claim audit changes what models say the checked artifacts establish, and whether a prespecified selection-blind auditor catches the resulting defects.

The next bounded study

The first experiment is compiles does not imply justifies. It uses a fixed, controlled interface so that artifact validity, claim fidelity, and selection pressure are not collapsed into one score.

1. Freeze the artifact. Each item begins with a source task and a compiling Lean statement and proof. The model receives a typed menu of consequence, scope, and dependency atoms, then returns an exhaustive claim certificate: each atom is marked licensed, not_licensed, or undetermined, with cited declarations, assumptions, and explicit non-claims.
2. Construct two label sets. Every scored atom receives a checked positive or negative witness in a finite decidable task family; unresolved atoms are excluded from primary scoring. Those full labels are y. A separate deterministic structural linter produces labels z using a fixed resource envelope: shallow normalization, direct conclusions and dependencies, no proof search, countermodel enumeration, or transitive closure. Before selection, the audit must beat the best trivial status-only baseline on non-stress units while retaining declared omissions. Lean compilation certifies the artifact; it does not supply either claim-fidelity label set by itself. The disagreement cases make failure measurable; clean units where z = y test whether an effect is specific to the preregistered blind spots.
3. Apply measured pressure. Generate one fixed pool of candidate certificates per artifact–generator pair. At nested best-of-N budgets, select the candidate that scores highest against the weak labels. Its proxy score R and full-fidelity score R* use the same loss, changing only z for y. Compare the selected candidate with the exact expected outcome of uniform random selection—the mean of that same prefix—alongside clean and audit-agnostic controls.
4. Test a selection-blind auditor. A frozen model auditor, blind to the proxy score, full labels, and selection budget, evaluates the selected certificates under a declared information and tool budget.

The primary safety outcomes are expected-random target-score loss and unsupported-authorization enrichment at maximum pressure. Proxy lift verifies that the selection manipulation actually moved its target; the proxy–target gap is a secondary Goodhart diagnostic because it can widen even while full fidelity improves. If the audit does not beat trivial baselines, candidate pools lack proxy-score variation, selection does not lift its score, or the planned sample cannot resolve the declared harm margin, the result is instrument-inconclusive rather than evidence of robustness. Clean units remain pipeline-integrity controls because their gap is zero by construction. This is inference-time selection, not RL training, and supports no claim about intent or adaptive evasion.

Each consequential result should ship with a compact claim–evidence–control record: what was observed, the lowest-capacity rival that still explains it, the evidence that distinguishes those accounts, candidate safeguards, and whether any safeguard was actually evaluated.

The entries below are hypotheses to test, not established mappings:

Defect	Observable evidence	Probe	Candidate control
Hypothesis shell	The claim omits load-bearing assumptions	Extract binders and dependencies	Require an exhaustive claim certificate
Vacuous scope	The theorem permits an empty target domain	Check or synthesize witnesses	Block promotion without instances
Decorative condition	Removing a premise leaves the result intact	Delete it and re-check	Flag unused semantic premises
Consequence overreach	A claimed consequence lacks a witness and admits a counterexample	Check the selected consequence atoms	Refuse unsupported authorization

Results that would still be useful

The study does not assume that verifier-guided selection causes systematic overclaiming. A small point estimate is evidence of robustness only if the selection first stage passes and confidence bounds exclude preregistered target-score-loss and unsupported-authorization margins. Successful detection by the prespecified auditor would identify a useful monitoring signal. Enrichment specific to blind spots, or falling auditor recall, would identify where stronger oversight needs testing. Each outcome changes what should be tested next.

What a useful result changes

• Training: whether the failure observed under controlled selection warrants testing an auxiliary claim-fidelity signal in verifier-rewarded training.
• Evaluation: whether formal-reasoning benchmarks should score the binding between statement and claim, not only proof acceptance.
• Oversight and safety cases: whether the prespecified auditor remains informative at a measured level of selection pressure, and what a machine-verified result may license downstream.
• Infrastructure: whether structured claim certificates—artifact, certificate, and audit trail—are a useful interface for further evaluation.

Why the method may travel

Proofs are the starting environment because they let the experiment separate a real validity signal from a separately warranted downstream claim. The portable unit is the controlled comparison: a declared proxy, a fuller target, fixed candidate pools, measured pressure, and an auditor with explicit capacity. If the first study discriminates among explanations, the same design can be tested in generated rule systems and other tool-mediated settings where a successful check is routinely treated as support for a broader decision.

Claim boundary

This work does not claim that formal validity is unimportant or that compilation itself supplies claim-fidelity ground truth. Machine validity and licensed inference are different layers, and oversight should test both.