I ran the same prover against the same 200 problems twice, one week apart, and the pass rate moved 12 points. Same model. Same prompts. Same problem set. The only thing that changed was the machine and the mathlib pin, and I hadn't written either of those down because nobody told me they were part of the experiment.
That is the sixth lesson in automated theorem proving that no paper appendix teaches you: the harness is the experiment. You can pick the right frontier model, engineer beautiful prompts, and benchmark on miniF2F like everyone else, and your number will still be a fiction if you can't say precisely what happened between "send the problem to the LLM" and "count it as solved." I learned this the expensive way — by publishing a comparison I could not reproduce, and then spending a month figuring out why.
The five lessons you already got
Someone has already told you to use a capable model. Someone told you prompting matters. Someone told you to use a standard dataset so your results mean something. Someone told you to sandbox the code so a hallucinated import can't wreck your host. Someone told you to log everything.
All true. All insufficient. Every one of those lessons treats the model as the object of study and the plumbing as a solved detail. But when you compare two proof-generation strategies, you are not comparing two models. You are comparing two full pipelines, and the pipeline has more free parameters than the prompt does. If you don't pin them, they move on their own, and they move between your two runs, which is exactly when you least want them to.
So let me trace one proof attempt through the whole mechanism, in the order it actually happens, and show you where the number leaks out.
What happens first: the call
You hand the system a Lean theorem statement with its goal unproven. Before any model sees it, your harness has already made decisions you probably didn't make consciously.
It decided how to format the statement into a prompt. It decided whether to include the surrounding file context, the available hypotheses, the imports. It decided the sampling temperature, the number of attempts, whether attempts run in parallel or sequentially with feedback from failed compilations fed back in. An agentic loop that retries with the compiler's error message is a fundamentally different experiment from a single-shot generation, and both get reported as "we used Claude."
Here is where the first silent variance enters. Two harnesses calling the same model API can differ in retry budget, context window usage, and whether they strip or keep the by tactic block. I once compared two "single-shot" setups and found one of them was quietly doing three samples and taking the best. It wasn't cheating. It was a default in a config file I inherited and never read.
The rule that saved me: the invocation is data. The prompt template, the sampling parameters, the attempt count, and the feedback loop all belong in the run record, not in your memory of what you probably did.
What happens next: the sandbox
The model returns a candidate proof — a string of Lean tactics. Now that string has to compile against a real Lean toolchain, and this is where most of your leaked variance lives.
Lean and mathlib move fast. A proof that closes cleanly against one mathlib commit can fail against the next because a lemma got renamed, a simp set changed, or a tactic's default behavior shifted. If your two runs used different mathlib pins — and they will if you ran lake update between them, which I did — you are measuring the library churn as much as the model. My 12-point gap was mostly this. One run compiled against a mathlib from three weeks earlier, and a cluster of omega and simp proofs that passed in the old library timed out or errored in the new one.
Then there's the timeout. "Verified in under 300 seconds" and "verified in under 60 seconds" are different benchmarks, and a busy CI runner with four proofs compiling in parallel gives each one less CPU than a quiet laptop does. Wall-clock timeouts on shared machines are not reproducible. I had a proof that passed on my laptop and failed in the container because the container capped it at 2 cores and elaboration ran long.
This is the part where a containerized, isolated run per attempt earns its keep — not because sandboxing is a security nicety, though it is, but because a container is the only honest way to freeze the toolchain, the library pin, and the resource ceiling into something you can hand to another person and say run this. The sandbox isn't protecting your host. It's protecting your claim.
The record you need out of this stage:
- Exact Lean toolchain version (
lean-toolchainfile, not "latest") - Exact mathlib commit hash, not a branch name
- Timeout as CPU time or a fixed core count, not wall-clock on shared hardware
- Memory ceiling, because OOM kills read as failures and skew the rate
What happens last: scoring
The proof compiled. Now you decide whether it counts, and this is the step where honest people accidentally lie.
The clean answer: a proof counts if Lean's kernel accepts it with no sorry, no admit, no native_decide you didn't intend to allow, and no unproven axioms sneaking in through axiom declarations. The kernel is the arbiter. If it type-checks the term without holes, it's a proof.
The unclean answers are everywhere. Some harnesses grep the output for "no errors" and miss a lingering sorry in a helper lemma. Some count a proof that closes the main goal but leaves a side goal open. Some allow native_decide, which trusts the compiler rather than the kernel — legitimate for some purposes, but a different, weaker guarantee, and mixing it into a pass rate without saying so inflates the number against provers that don't use it. I have seen partial-credit scoring reported next to strict scoring in the same table, with no column telling you which was which.
Verification has to run in the same frozen environment as compilation, and the pass criterion has to be one sentence you can state out loud. Mine is: the kernel accepts the full statement with no sorry and no unpinned axioms. If you can't say yours that plainly, you don't have a benchmark, you have a vibe.
What the common interface actually buys you
For a while I built a custom adapter for every prover I wanted to compare — one for the agentic loop, one for the single-shot baseline, one for the tree-search thing a colleague sent me. Each adapter made its own quiet decisions about prompting, timeouts, and scoring. That's not comparison. That's three separate experiments wearing a trench coat.
The reason to run every strategy through one interface — same prompt-delivery contract, same sandbox spec, same scoring rule, with only the strategy swapped — is not that it saves you integration work, though it does. It's that comparability is only real when the sole variable is the thing you claim to be studying. Everything else has to be identical by construction, not by your best recollection of last Tuesday's run.
A reproducibility checklist you can act on
| Stage | Pin this | Common failure |
|---|---|---|
| Call | prompt template, temperature, attempt count, feedback loop | "single-shot" that quietly samples 3x |
| Sandbox | Lean toolchain + mathlib commit hash | lake update between runs |
| Sandbox | CPU cores + memory + timeout | wall-clock on a shared runner |
| Scoring | kernel accept, no sorry, axiom policy | grep for "no errors" |
This week
Take your last benchmark run and try to reproduce one number — a single prover's pass rate on a single dataset — from nothing but your recorded config. No memory, no "I think I used." If you can't rebuild the container, the mathlib pin, and the scoring rule from what you wrote down, that's your first bug, and it's bigger than any prompt you were about to tweak.
You are not measuring the model until everything around the model holds still.
