Don’t trust the read. Re-run the proof.
Our whole claim is that you shouldn’t have to trust us. So here are the machine-checked proofs — clone the repo, build them, and print the axioms yourself. And here, first, is exactly what they do NOT prove.
What these do not proveThese certify the linear algebra — the erasure and the recovery mechanism, the second now exact under the model’s real activation gate. They do NOT certify the detector, the measured rate, or that any of it generalizes to real models. That answer is empirical, and it lives on the scored record — not here. The scored record →
The two things a skeptic can’t wave away.
A proof you wrote can be dismissed as a proof you tuned. These two can’t: someone else re-ran one, and the other is the exact failure the skeptics fear — reproduced, on purpose.
Anyone can write a proof that only ever checks their own homework. The real test is whether a stranger with no stake can pull the repo, run the checker, and get the same green light — on their own proof routes, not yours.
We left three theorems open as a challenge. Justin Garringer (CarlSR9001) proved all 3 on 2026-07-22 — his own routes, checker-verified, standard axioms only. He engaged voluntarily; no bounty was set. Independent reproduction is the answer to “the check just manufactures confidence.”
commit cb2dc14receipt fa72179a3011…You’re right, and it’s the whole reason we exist. So we built the trap on purpose: one model whose headline number climbs while a guarded ability quietly rots — shipped, so you can watch a “better” score hide a worse model.
whetstone-pair — gemma-2-2b-it-base vs the same model, the same base, LoRA-fine-tuned on CodeAlpaca (deterministic, greedy decode). The headline metric goes up; a guarded ability quietly erodes. The score improved and the artifact got worse — a deterministic recipe, shipped, of exactly the trap a good reviewer distrusts.
Three tiers, 3 standard axioms, zero sorry.
Each tier certifies its linear algebra — and states its own ceiling in the same breath. Not the detector; not the measured rate; not that it generalizes. Click any theorem to see what it actually proves, in plain words.
Proofora/Excise.leanThe surgery. An operation that removes exactly one subspace from a model’s weights — and provably leaves everything else untouched.
the reversible-erasure linear algebra — a symmetric projector that removes exactly the register subspace
survives_iff_fixedwhat you keep is left untouched
A reading that lies outside the removed subspace passes through the erasure completely unchanged.
Why it matters — This is the guarantee the excision is surgical: it cannot damage anything it wasn’t aimed at.
erased_on_kernelwhat you remove is gone cleanly
The removed component is zeroed exactly — it contributes nothing to any surviving reading.
Why it matters — The thing you meant to remove is actually gone, not merely turned down.
registerLock_isProjectorthe eraser is a real projector
The eraser (I − R Rᵀ, with orthonormal columns) is a genuine projector: symmetric, and applying it twice equals applying it once.
Why it matters — That stability (idempotence) is what makes the operation well-defined — re-applying it introduces no drift or side-effects.
rank_one_erases_only_spanone vector can’t fake a full removal
A rank-1 removal can only erase a target that lies along its single direction — so one witness vector can never remove a whole subspace.
Why it matters — A provable floor on evidence: you cannot pass off a single direction as a complete excision.
Proofora/RefutersWall.leanThe open challenge. The same removal math, left open for any outsider to break, plus the identities that pin down exactly what it erases — proved both directions.
an open challenge lane — the rank / kernel identities behind the register-lock, left open for anyone to break
tierA_false_claim_is_refutedthe checker rejects what’s false
A deliberately false claim is machine-refuted — the checker actively rejects what’s wrong, not merely accepts what’s right.
Why it matters — A checker that can only ever say “yes” proves nothing; this shows it says “no” when it should.
registerLock_kernel_eq_rangeerases exactly the target — no more, no less
The set the operation erases is exactly the intended subspace: nothing outside it is touched, and nothing inside it survives.
Why it matters — Exactness in both directions — no collateral damage, and no leftover remnant of what was removed.
registerLock_rankremoves exactly k dimensions (the sealed target)
The rank-k excision removes exactly k dimensions — the erased subspace has precisely the intended size.
Why it matters — This was the hardest of the three challenge targets — the one a stranger crossed with his own proof.
charge_in_rowspace_of_vanishing_on_kerthe converse — the survivor set is pinned down
If a reading vanishes on the erased subspace, it must lie entirely within the surviving row-space — the converse direction.
Why it matters — Together with its partner theorem, this closes the identity both ways: the survivor set is this and nothing else.
Proofora/RegisterBurial.leanThe confession. Why a planted payload is invisible when the model sits at rest, separates the instant a trigger fires, and can be recovered exactly — now proved under the model’s real activation.
the register-burial payload-recovery identity is exact even under the model's real activation gate — a certified MECHANISM, not the detector, not the rate, not that it generalizes to real models
onFireEval_eq_atthe setup is consistent, not special-cased
The fixed-trigger evaluation is exactly the general evaluation at the trigger setting.
Why it matters — It rules out a special-cased trick: the headline result is just an instance of the general one.
cold_collisionat rest, payload and no-payload look identical
Two weight sets — one carrying a hidden payload, one carrying none — produce an identical ordinary reading. At rest they are indistinguishable.
Why it matters — This is the blindness a backdoor relies on: inspecting the model normally cannot see the difference.
onfire_separatesunder trigger, they separate
On a triggering input, those same two weight sets read differently — what was identical at rest separates.
Why it matters — The payload is invisible until the trigger fires — exactly what makes it dangerous, now made formal.
register_burial_separationa buried payload is real and trigger-only
There provably exist weights where the ordinary reading is blind but the triggered reading separates the payload out.
Why it matters — The whole threat model in one statement: a buried payload is both real and visible only under trigger.
recovery_exactthe payload is recovered exactly, not estimated
Across the whole family of such constructions, the hidden payload is recovered exactly — an identity, not an approximation.
Why it matters — Not “we estimate the payload” — the recovered value provably equals the planted value.
recovery_exact_activationstill exact under any activation
That exact recovery still holds under an arbitrary activation, not just an idealized one.
Why it matters — The first idealization is removed — the result survives a realistic gate, not only a toy.
silu_posthe lemma under the crown result
On a triggering pass, the real SiLU activation is strictly positive.
Why it matters — A small, necessary step that lets the exact-recovery proof go through under the real activation.
recovery_exact_siluexact even under the real SiLU gate — the crown
Exact recovery holds even under the real SiLU activation a model actually uses — every idealization now removed.
Why it matters — The crown result: recovery isn’t an artifact of a simplified model; it holds under the real gate.
Four questions worth clicking.
Everything above in plain words — tap a question.
What even is a “machine-checked proof”?
A person can wave their hands; a proof assistant can’t. Each claim is written in Lean — a language where the computer refuses any step that doesn’t strictly follow. If it compiles, every line has been checked by a machine with no interest in agreeing with us. “Trust me” never enters.
What does “zero sorry” mean?
`sorry` is Lean’s escape hatch — “assume this part, I’ll fill it in later.” A single `sorry` anywhere turns the whole thing into a promise instead of a proof. Zero `sorry` means there are no holes: every claim is discharged all the way down.
Why do the “three standard axioms” matter?
Every proof starts from some assumptions. Ours start from exactly the three that mainstream mathematics already uses — and nothing else. You can print that list yourself with `#print axioms`. If we had smuggled in a convenient extra assumption, it would appear there. It doesn’t.
It’s just linear algebra — what’s that got to do with a backdoor?
A backdoor lives in a model’s weights, and weights are matrices. These claims are about what an operation on those matrices provably does: an excision removes exactly one subspace and nothing else, and a payload hidden from a normal read is recoverable exactly under trigger. The proofs certify the mechanism is sound. Whether it catches real backdoors in the wild is a separate, empirical question — and those numbers live on /coverage, not here.
Two minutes, on your own machine.
[propext, Classical.choice, Quot.sound] and nothing elsegit clone https://github.com/Vulcora/proofora && cd proofora lake exe cache get && lake build # then, per theorem: lake env lean <(echo "import Proofora\n#print axioms Proofora.RegisterBurial.recovery_exact_silu")github.com/Vulcora/proofora →
This certifies the mechanism — it is not the empirical answer. Whether the read generalizes is a question of numbers, not theorems, and the numbers are posted in full: the per-scanner board across all seven models on the reveal board, the scored capability record with its conceded failures on /coverage, and the open challenge. We don’t let the proof stand in for the table.
The proof is the floor. The record is the case.