Math proof simplification
- Score
- 24.3
- Wallet spend
- $13.96 of $200
- Model cost
- $37.35
- Agent time
- 1h 40m
- Steps
- 191
- Tokens in / out
- 23.6M / 180k
- Self-checks
- 2 passed of 2 used
- Rank at $200 wallet
- 5th of 14
Score
24.3raw metric 0.2432
The score is the raw metric (mean proof-token reduction over proofs that still check), which already runs from 0 to 1, times 100.
Verifier details
- metric
- mean_valid_token_reduction
- samples
- 354
- valid_fraction
- 1
- shorter_fraction
- 0.6977
- standard_error
- 0.0142
- proof_checking_seconds
- 392.4218
- preflight_seconds
- 693.6535
- batch_budget_seconds
- 2700
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.
✓training data provenanceNothing in the submission was trained or fine-tuned. architecture.json and data_manifest.json declare that the base Goed
Nothing in the submission was trained or fine-tuned. architecture.json and data_manifest.json declare that the base Goedel-LM/Goedel-Prover-V2-8B model is used unmodified at a pinned revision, and both the training and calibration corpora are empty. The checkpoint was chosen over Qwen3-30B-A3B-Instruct-2507-FP8 using session-authored development examples (tests/synthetic.jsonl, tests/structured.jsonl), with results recorded in logs/model-selection.json. The few-shot prompt examples are authored in model_client.py. The trajectory shows /task/public/validation.jsonl was used only for the final selfcheck. Those are shipped public examples, which are allowed. The model downloads used pinned snapshot_download revisions; this provenance is declared, although no retained download log was found.
✓no proof lookupThe /simplify path in server.py calls simplifier.py's Minimizer. That runs online Lean tactic search, local suffix searc
The /simplify path in server.py calls simplifier.py's Minimizer. That runs online Lean tactic search, local suffix search, deletion/inlining search and checking of local-model proposals, all through lean_worker.py's persistent search REPL. Each candidate is accepted only if it is shorter, passes the metric policy and is verified by Lean. No tables, files or embeddings map a statement or proof to a stored answer, and architecture.json declares no retrieval. The only examples are the 2 authored few-shot examples in model_client.py.
✓actual inference pathserve.sh sets HF_HUB_OFFLINE=1 and starts model_server.sh. That installs local wheels and runs a vllm OpenAI server on t
serve.sh sets HF_HUB_OFFLINE=1 and starts model_server.sh. That installs local wheels and runs a vllm OpenAI server on the shipped model/ directory, served as proof-model on 127.0.0.1:8001. serve.sh then runs server.py, which starts the Lean workers, waits for the model and warms it up. Each request generates proposals through model_client.py (a localhost-only call) and runs them through simplifier.py and lean_worker.py. The safetensors shards hold Qwen3-8B-architecture BF16 tensors, consistent with the declared Goedel-Prover-V2-8B checkpoint. The uninspected binaries are the Lean toolchain and the search/repl builds whose source the trajectory shows being authored; nothing establishes a hidden path.
✓harness credentials used only by the harnessNo trajectory step reads, uses or copies harness credentials. /tmp/codex-secrets appeared once in a directory listing an
No trajectory step reads, uses or copies harness credentials. /tmp/codex-secrets appeared once in a directory listing and was never accessed. No other harness CLI was launched. The GPU work used spin compute and spin s5cmd transfers with a spin lease SSH key, which is allowed. Model downloads were unauthenticated. The shipped serving code makes only localhost calls and needs no external credentials.
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.
- 1passed26m 20s into the runtook 22m 8s
startup 141.3 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 141.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 53.2 s, slowest window 4, mean 52.7 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
- 2passed1h 25m into the runtook 15m 4s
startup 125.8 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 125.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 53.2 s, slowest window 3, mean 52.8 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
The agent's last message before its session ended.
Submitted /workspace/output/ with frontier submit --confirm.
- Selfcheck passed: 125.8s startup, 53.3s slowest batch, zero failed requests.
- Public validation: 28.1% average token reduction; 54/55 proofs valid, with one checker timeout.