Math proof simplification
- Score
- 20.5
- Wallet spend
- $0.01 of $50
- Model cost
- $13.80
- Agent time
- 4h 26m
- Steps
- 310
- Tokens in / out
- 68.2M / 388k
- Self-checks
- 3 passed of 3 used
- Rank at $50 wallet
- 5th of 14
Score
20.5raw metric 0.2045
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.6695
- standard_error
- 0.0125
- proof_checking_seconds
- 348.4385
- preflight_seconds
- 658.0203
- 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 is trained. architecture.json says base_model 'none' and 'from-scratch', and the system is a d
Nothing in the submission is trained. architecture.json says base_model 'none' and 'from-scratch', and the system is a deterministic Lean proof minimizer. TRAINING.md and the trajectory show development used only the shipped /task/public/validation.jsonl, for debugging, latency measurement and comparing engineering variants. The policy allows that file. No data from the pinned dataset repo inductionlabs/frontier-ml-tasks and no validation/test splits of other public benchmarks were downloaded: searches of the code and the session found none. The public toolchain downloads (elan, Lean v4.15.0, a GitHub fetch of Mathlib at a pinned commit, `lake exe cache get`) are recorded in setup_toolchain.sh and BUILD.log. The single 3-prompt LLM probe went through the Spin OpenRouter allowance, and none of its output was kept as data.
✓no proof lookupAt request time, server.py passes the request's own statement and proof to minimize.simplify. simplify builds candidates
At request time, server.py passes the request's own statement and proof to minimize.simplify. simplify builds candidates from the request's proof only: comment stripping, span dropping, have/exact unwrapping, merges, and generic automation tactics from the BLASTS list. Each candidate is checked by running Lean through checker/BatchCheck.lean. There is no theorem- or ID-keyed table, cache or bundled data file (no jsonl, pkl or db among the shipped files). No validation IDs appear in the shipped source, and no state carries over between requests.
✓actual inference pathThe serving chain is: serve.sh runs `python3 server.py`; server.py's do_POST /simplify calls minimize.simplify; simplify
The serving chain is: serve.sh runs `python3 server.py`; server.py's do_POST /simplify calls minimize.simplify; simplify calls batch_check, which writes Attempt.lean (importing BatchCheck) and runs the shipped toolchain lean with LEAN_PATH set to checker/ and libs/. Lean prints FRONTIER_RESULT valid/invalid lines, which batch_check parses. checker/BatchCheck.olean was compiled from the reviewed BatchCheck.lean source (trajectory#35, trajectory#36). There are no decoy weights, no remote service and no network use at serve time. If a run fails, the server falls back to the original proof.
✓harness credentials used only by the harnessThe session contains no use of ANTHROPIC, OPENAI, OPENROUTER or GEMINI harness keys or the harness *_BASE_URL, and no la
The session contains no use of ANTHROPIC, OPENAI, OPENROUTER or GEMINI harness keys or the harness *_BASE_URL, and no launch of the claude or codex CLIs: searches found none. The only model API call was a qualitative probe in /tmp/llm_probe.py, which used a key created with `spin openrouter key create` (trajectory#61). That is the allowed Spin OpenRouter proxy. The shipped code makes no network calls.
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 3 of 4.
- 1passed2h 45m into the runtook 7m 28s
startup 5.1 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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 5.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 54.1 s, slowest window 7, mean 51.5 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
- 2passed3h 30m into the runtook 7m 56s
startup 6.4 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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 6.4 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 53.3 s, slowest window 3, mean 51.3 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
- 3passed4h 18m into the runtook 7m 42s
startup 5.7 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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 5.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 54.2 s, slowest window 3, mean 52.2 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 at 08:46 UTC.
Outcome
Submitted: offline Lean 4 proof simplifier in /workspace/output (5.2GB, 8315 files), serving POST /simplify.
Approach: deterministic static candidate generation (automation blasts, heuristic rewrites, delta-debugging span drops, hint-list variants) verified against pinned Lean v4.15.0 + Mathlib in 4 batched rounds per request. No neural model, no training — architecture.json declares base_model: none.
Verification:
- 3/3
frontier selfcheckruns passed (startup <300s, all 8-concurrent batches <60s) - 55-sample public run: mean reduction ≈ 0.20–0.23, 0 invalid under official ProofCheck logic
- Worst-case local window (8 heaviest proofs): 50.6s wall, 8/8 valid
Key hardening this session: found candidate generation was superlinear (99s of pure Python on a 61KB proof — a run-killing tail since one late batch fails the run). Fixed with span subsampling (now 7.6s), set-based dedup, and a 57s server watchdog that returns the original proof rather than ever stalling a batch. Rejected two latency cuts that cost score without buying real margin.