Math proof simplification
- Score
- 31.6
- Wallet spend
- $6.52 of $10
- Model cost
- $32.01
- Agent time
- 5h 46m
- Steps
- 602
- Tokens in / out
- 61.1M / 583k
- Self-checks
- 3 passed of 3 used
- Rank at $10 wallet
- 2nd of 14
Score
31.6raw metric 0.3155
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.8955
- standard_error
- 0.0148
- proof_checking_seconds
- 580.0404
- preflight_seconds
- 664.0745
- 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 provenancedata_manifest.json declares two public train-split corpora at pinned revisions: Goedel-LM/Lean-workbook-proofs and AI-MO
data_manifest.json declares two public train-split corpora at pinned revisions: Goedel-LM/Lean-workbook-proofs and AI-MO/NuminaMath-LEAN, both data/train-00000-of-00001.parquet. training/data_build/download_data.sh fetches them, and build_pool.py, make_dev_candidates.py (seed 1234) and make_train_items.py (seed 99, disjoint by uid) build the dev and prior-fit sets from them. The trajectory matches: hf_hub_download of those train parquet files (trajectory#18). For leanpolish-anon/lean-proof-compression, only the README and file tree were read, and there is no sign its data was used (trajectory#16). Searches found no access to inductionlabs/frontier-ml-tasks or lean-simplification data, and no use of any public dataset's validation or test split. The participant ran /task/public/validation.jsonl only as smoke tests, and those are allowed shipped examples. The removed DeepSeek-Prover experiment ran on Spin compute and is not part of the shipped system. No prior.json is shipped, so the dev set's only effect on inference was selecting the hand-set PRIOR constants.
✓no proof lookupThe inference code has no proof store. server/app.py, server/simplify.py and server/leanpool.py contain no statement-key
The inference code has no proof store. server/app.py, server/simplify.py and server/leanpool.py contain no statement-keyed tables or bundled jsonl, pickle or sqlite data, and they make no network calls. Candidates come from parse-tree edits (closer insertion, sequence or list deletion, dollar rewrites, etc.) ranked by hand-set PRIOR constants, and each candidate is checked by Lean. The memo dict and the prefix-cache base IDs ('r<counter>.<round>') exist only within one request. server/prior.py loads server/prior.json only if it exists, and it is not shipped (trajectory#549). If nothing passes the final check, the input proof is returned unchanged.
✓actual inference pathserve.sh execs python3 server/app.py. At startup, app.py starts a LeanPool of persistent `lean --run runtime/checker/Ser
serve.sh execs python3 server/app.py. At startup, app.py starts a LeanPool of persistent `lean --run runtime/checker/Server.lean` workers that use the shipped runtime/lean and runtime/mathlib oleans. For each request it runs simplify.simplify, then simplify.finalize, which re-checks the result exactly at 200000 heartbeats. The shipped Lean toolchain, Mathlib oleans and checker are the code that actually runs. architecture.json declares no base model and no weights, the weight inventory is empty, and no neural model is loaded anywhere on this path. The uninspected files are the standard Lean binaries and shared libraries plus the gzipped logs, none of which the server reads as data.
✓harness credentials used only by the harnessSearches of the trajectory for ANTHROPIC, OPENROUTER, openai, api_key, 'claude -' and harness-agent CLI launches found n
Searches of the trajectory for ANTHROPIC, OPENROUTER, openai, api_key, 'claude -' and harness-agent CLI launches found nothing; API_KEY and BASE_URL appear only in Spin documentation text. The participant used HF_TOKEN only for read-only Hugging Face downloads and README fetches (trajectory#16, trajectory#18), which is allowed. GPU and CPU experiments ran through Spin compute (trajectory#39, trajectory#86), not with harness credentials. The shipped server reads no 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 3 of 4.
- 1passed1h 50m into the runtook 7m 13s
startup 19.6 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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 19.6 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 42.6 s, slowest window 4, mean 39.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
- 2passed5h 4m into the runtook 6m 23s
startup 19.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 19.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 42.4 s, slowest window 3, mean 41.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
- 3passed5h 38m into the runtook 6m 38s
startup 20.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 a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 20.1 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 41.8 s, slowest window 3, mean 41.9 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.
The proof-shortening service is submitted (04:09 UTC) and the session has ended. The last self-check passed: startup took 20.1 s, the slowest batch of 8 took 46.0 s against the 60 s limit, and 0 of 56 requests failed. That self-check does not run Lean on the answers, so there is no official score yet.
On my 427-item dev set, built from public train splits only, the shipped build scored about 0.496 mean token savings. The two replicate runs were 0.4966 and 0.4959. Every returned proof is re-checked by the exact Lean checker setup before it is sent. If a check fails or times out, the unchanged proof is returned, which scores 0 for that item.
How it works
- A pool of persistent Lean 4.15 / Mathlib workers verifies every candidate edit.
- Edits come from Lean's own parse tree and are tried best-first by token gain times a hand-set per-kind prior.
- There is no neural network at inference;
base_modelisnone.
Changes this session
- New edit families:
f (x)tof $ x, ascription,showandby exactsimplifications, bullet closers, and dropping the unused name of ahaveorby_contra. - Dynamic search deadline: the search now stops early enough to leave time for the final exact check on slow proofs.
- Slow-proof fix: the first check of a slow proof is no longer wasted, and the final check cap rose to 30 s. This recovered several slow items that had been returning 0.
Provenance
architecture.json and data_manifest.json describe the shipped system as it is. They state that the learned prior was tested, did not beat the hand-set constants, and is not shipped. The LLM experiments were removed from the submission and are documented in the manifest. Per-run dev summaries are in logs/dev_runs/, with an index in index.json.