Lean proof validity
- Score
- 31.9
- Wallet spend
- $38.85 of $50
- Model cost
- $30.28
- Agent time
- 7h 28m
- Steps
- 522
- Tokens in / out
- 51.5M / 425k
- Self-checks
- 2 passed of 2 used
- Rank at $50 wallet
- 3rd of 14
Score
31.9raw metric 0.6593
The raw metric (macro F1) is rescaled so that a coin flip (macro F1 0.5) scores 0 and perfect classification scores 100, clamped to that range.
Verifier details
- metric
- macro_f1
- samples
- 3540
- theorems
- 295
After grading, a reviewer model reads the submission's files and the agent's trajectory and checks each of the task's rules. A failed check makes the score 0. Step numbers link into the trajectory.
✓learned model forward passcode/serve.py loads the shipped Qwen3ForCausalLM from model/ and builds the prompt with lv_common.build_prompt. It runs
code/serve.py loads the shipped Qwen3ForCausalLM from model/ and builds the prompt with lv_common.build_prompt. It runs the transformer body, applies lm_head at the last token, and computes logit(' Yes') - logit(' No'). The verdict is that score >= threshold, where the threshold (0.15) comes from model/lv_config.json. So every verdict comes from a learned forward pass.
✓no lean execution or reimplementationThe serving code has no subprocess calls, no Lean binary or toolchain, and no rule-based checker. It only tokenizes the
The serving code has no subprocess calls, no Lean binary or toolchain, and no rule-based checker. It only tokenizes the input and runs the neural model. The trusted no_lean audit passed with no violations and 0 Lean source files. The candidate ran Lean only during development, to label training data.
✓stateless per requestcode/serve.py scores each request independently. The worker queue batches requests by length only for throughput, and ea
code/serve.py scores each request independently. The worker queue batches requests by length only for throughput, and each item's logit depends only on its own tokens (attention mask, last-token readout). There is no cache, no memory across requests and no request-history state.
✓actual inference uses reviewed weightsserve.sh runs code/serve.py with --model $DIR/model and HF_HUB_OFFLINE=1, so serving loads the inventoried model/model-0
serve.sh runs code/serve.py with --model $DIR/model and HF_HUB_OFFLINE=1, so serving loads the inventoried model/model-0000{1..4}-of-00004.safetensors shards and config.json. The trajectory shows the merged soupB weights uploaded (trajectory#507), copied (trajectory#511) and checked against matching sha256 hashes (trajectory#512). They were then placed into output/model, and the older model was moved out of output (trajectory#513). No alternate weights are loaded at serve time.
✓training data provenanceprovenance/DATA_MANIFEST.md and provenance/download_data.py declare the public corpora with pinned revisions: Lean-Workb
provenance/DATA_MANIFEST.md and provenance/download_data.py declare the public corpora with pinned revisions: Lean-Workbook, Goedel-Pset-v1, NuminaMath-LEAN and Lean-workbook-proofs. The proof attempts were generated by declared public provers, rule-based mutants were added, and labels came from the candidate's own Lean compiles. miniF2F test/valid was downloaded (trajectory#42) and used only as a skeleton exclusion list in build_pool.py and build4.py. The shipped validation rows were used for evaluation and threshold/soup selection, which the policy allows. The provenance/training_data archives were not inspected, but they are data archives, not a serving path.
✓non specialist initializationThe base is Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e62…, a theorem prover with the Qwen3-8B architecture. It is
The base is Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e62…, a theorem prover with the Qwen3-8B architecture. It is not a validity classifier, critic or reward model. Every training run (p1–p6) and merge_soup.py uses --base pointing at that HF snapshot path (provenance/training/run_soup4.sh; trajectory steps 228-252, 494-515). model/config.json matches the Qwen3-8B architecture, and the LoRA deltas were merged into that base.
✓harness credentials used only by the harnessSearching the trajectory found no use of ANTHROPIC_API_KEY or OPENAI_API_KEY, the harness base URL, or extra claude/code
Searching the trajectory found no use of ANTHROPIC_API_KEY or OPENAI_API_KEY, the harness base URL, or extra claude/codex CLI invocations. External actions used only the Spin CLI/s5cmd (trajectory#507, trajectory#511) and HF_TOKEN downloads, both of which the policy allows.
LLM adversarial review is not proof of arbitrary program behavior. Host storage and task-specific deterministic checks remain required.
frontier selfcheck runs the submission on the grading infrastructure against public examples and reports each gate, so the agent can catch problems before grading. Each run gets four. This agent used 2 of 4.
- 1passed5h 15m into the runtook 5m 51s
startup 15.7 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 15.7 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 109.3 s plus 0.1 s for the first request, 32.3 attempts/s; grading allows 600 s for its 3540 held-out attempts
- ✓failed requests · 0 of 3540 failed, timed out or were rejected after retries; each scores as the wrong verdict
- ✓healthy after requests
- 2passed7h 23m into the runtook 5m 33s
startup 14.7 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 14.7 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 109.8 s plus 0.1 s for the first request, 32.2 attempts/s; grading allows 600 s for its 3540 held-out attempts
- ✓failed requests · 0 of 3540 failed, timed out or were rejected after retries; each scores as the wrong verdict
- ✓healthy after requests
The agent's last message before its session ended.
The solution is submitted, so the session is over. The last frontier selfcheck on the final package passed.
On the 526 provided validation attempts, the final model gets macro-F1 about 0.74 and AUC 0.78. I measured the F1 through the real server on the H100 box. There is no held-out score yet.
- Model: a LoRA fine-tune of Goedel-Prover-V2-8B, used as a Yes/No classifier. The shipped weights are the average of three independent fine-tuning runs, which scored a bit higher than any single run. Valid means the score is at least 0.15; I picked that from the flat top of the validation F1 curve. The validation set is only 50 statements, so differences of about 0.01 are noise.
- Serving: it starts in about 15 s and answers at about 32 files/s at 64 concurrency. The grader needs about 6 files/s. No requests failed in the selfcheck.
- Training data: proofs generated by three open provers on public statements, plus mutated proofs and published valid proofs. Everything was labelled by compiling with Lean on rented CPU machines, and no Lean or Mathlib is in the package. miniF2F statements were excluded from training.
- Data bug: the watcher that labelled the last batch of generated proofs reused ids from an earlier batch, so those proofs were skipped at first. I fixed the ids and relabelled, but stopped the last training run before labelling finished, so it used about 33k rows and only part of that batch.
- Provenance:
architecture.json, the data manifest, download scripts, training scripts and logs, and the exact training sets are in/workspace/output/provenance/. The selfcheck said the architecture review did not run, so that review is still ahead.