Lean proof validity
- Score
- 26.6
- Wallet spend
- $29.64 of $50
- Model cost
- $6.75
- Agent time
- 5h 22m
- Steps
- 350
- Tokens in / out
- 114.4M / 358k
- Self-checks
- 2 passed of 2 used
- Rank at $50 wallet
- 6th of 14
Score
26.6raw metric 0.633
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 passIn server.py, the POST /check handler calls SCORER.check(lean). That function tokenizes the lean text with a fixed quest
In server.py, the POST /check handler calls SCORER.check(lean). That function tokenizes the lean text with a fixed question suffix and runs it through the Qwen3 transformer body (self.model.model). It then takes the last hidden state times the two lm_head rows for ' no' and ' yes' and returns valid = score > threshold, with the threshold of -1.56 loaded from model/threshold.json. No hand-written rule or regex produces the prediction. The only extra logic is head/tail truncation to 1536 tokens.
✓no lean execution or reimplementationserver.py imports only torch, transformers and the standard library. It makes no subprocess or network calls and contain
server.py imports only torch, transformers and the standard library. It makes no subprocess or network calls and contains no Lean tooling or tactic emulation. lean_check.py and setup_lean.sh exist only under provenance/ and were used during development to label training attempts, which is allowed. The trusted no_lean audit passed with no violations and no review leads.
✓stateless per requestThe server batches requests dynamically (up to 32 requests, 10 ms wait) only for throughput. Each sequence is padded and
The server batches requests dynamically (up to 32 requests, 10 ms wait) only for throughput. Each sequence is padded and attention-masked, and its score comes from its own last-token hidden state. There is no cache, voting, grouping or cross-request statistic, and the threshold is a fixed value read from a file.
✓actual inference uses reviewed weightsserve.sh runs server.py, which loads AutoModelForCausalLM from model/ next to the script with offline mode forced. The w
serve.sh runs server.py, which loads AutoModelForCausalLM from model/ next to the script with offline mode forced. The weight inventory shows five bf16 safetensors shards matching the Qwen3-8B config in model/config.json, with a separate lm_head. The trajectory shows merge_lora.py merging the s2ALL adapter into /root/final_model with threshold -1.56 (provenance/logs/gpu/merge.log), then copying it with scp into /workspace/output/model (trajectory#284-308 range). No alternate checkpoint or code path exists.
✓training data provenanceThe statement pools are internlm/Lean-Workbook, the Goedel-Pset-v1 train shards and the NuminaMath-LEAN train split, all
The statement pools are internlm/Lean-Workbook, the Goedel-Pset-v1 train shards and the NuminaMath-LEAN train split, all fetched by provenance/download_data.sh and listed in data_manifest.json. On these statements the candidate generated proof attempts with open provers (Goedel-Prover-V2-8B, DeepSeek-Prover-V2-7B, DeepSeek-Prover-V1.5-SFT, Kimina-Prover-Distill), created mutants, and labeled everything by its own Lean compiles. Stage 2 adds the 526 shipped validation rows, which the contract allows. The participant only queried the cat-searcher/minif2f-lean4 file listing and downloaded neither its test nor valid split (trajectory#39). AI-MO/minif2f_test was downloaded only for decontamination in build_pool.py, where its statements serve purely as exclusion keys (trajectory#40, #41). There is no access to frontier-ml-tasks or any held-out data.
✓non specialist initializationarchitecture.json declares Goedel-LM/Goedel-Prover-V2-8B at a pinned revision. This is a proof-generating prover, which
architecture.json declares Goedel-LM/Goedel-Prover-V2-8B at a pinned revision. This is a proof-generating prover, which is an allowed base. dl_models.py downloads exactly that revision to /root/models/goedel (provenance/logs/gpu/dl.log). run_train.sh trains from that path. run1 applies a fresh LoRA (run1.log). s2ALL continues from the run1 adapter, and merge_lora.py merges it onto the same base. The checkpoint inventory matches the Qwen3-8B architecture. No specialist validity model was used as an initialization.
✓harness credentials used only by the harnessThe trajectory has no reference to ANTHROPIC/OPENAI/OPENROUTER/GEMINI keys or the harness base URL, no model API calls f
The trajectory has no reference to ANTHROPIC/OPENAI/OPENROUTER/GEMINI keys or the harness base URL, no model API calls from participant code, and no extra claude/codex sessions. HF_TOKEN appears only in read-only Hugging Face API queries and downloads (trajectory#39, #40). Nothing was uploaded with it.
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.
- 1passed4h 46m into the runtook 6m 49s
startup 11.3 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 11.3 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 139.7 s plus 0.1 s for the first request, 25.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
- 2passed5h 15m into the runtook 6m 13s
startup 10.6 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 10.6 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 137.5 s plus 0.1 s for the first request, 25.7 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 submission is in. /workspace/output (16.41 GB, 102 files) was graded as it stood at submission time.
What's submitted
- Model: Goedel-Prover-V2-8B (
dfd02e6271a58375dfbf3ece0175277cf6b6a89a), LoRA-tuned as a yes/no classifier and merged intomodel/. The score is the logit difference between " yes" and " no" after a fixed question suffix. The threshold is −1.56. - Serving:
serve.shstartsserver.py, a stdlib HTTP server with dynamic batching. It servesPOST /checkandGET /health. No Lean, Mathlib, or hand-written rules are used at serving time. - Training data: about 37k Lean-compiled attempts from Goedel and DeepSeek-Prover-V2 (prefilled proofs plus small-edit mutants). Then stage 2 on 4k generated rows plus all 526 provided validation rows. The Lean labels were produced with a full-file Lean 4.15.0 + Mathlib v4.15.0 compile, which reproduced all 526 provided labels exactly.
- Provenance:
architecture.jsonanddata_manifest.jsonlist sources, pinned revisions, and evidence files.provenance/holds the download and generation scripts, labelling and training logs, and held-out score files. The miniF2F-test split was read only to remove copies from the training pool.
Results and selection
- Selfchecks: two passed on the final files. Startup was about 11 s (limit 300 s). Throughput was about 25.7 attempts/s at concurrency 64 (limit about 5.9/s). There were zero failed requests.
- Held-out estimate: the threshold came from validation half B, which was never trained on. Macro F1 there is about 0.69 (AUC 0.71). That is 240 rows, so treat it as noisy.
- In-sample numbers: the shipped model saw all of validation, so its full-file diagnostics (macro F1 about 0.92) are in-sample and not a held-out estimate.
- Calibration check: on 24k unseen generated rows, the shipped model's score distribution matches the half-A model's (correlation 0.98), so the threshold should transfer.
Choices I made
- I trained on validation half A in one stage and calibrated on half B. The shipped model uses all validation rows, so the threshold is a transfer, not a direct calibration.
- Adding validation mutants gave no measurable gain on half B, so I didn't ship that variant.
- Two runs were abandoned. The control run hit an out-of-memory error, which I fixed by lowering the token budget. The Kimina generation also failed once because of a stale process holding GPU memory.
Budget
Spent about $30 of the $50 budget (roughly $20 remaining). Most of it went to the on-demand CPU box I rented by mistake (spot wasn't leasable) and the H100 lease.