Math proof simplification
- Score
- 14.3
- Wallet spend
- $0.00 of $10
- Model cost
- $9.20
- Agent time
- 3h 2m
- Steps
- 198
- Tokens in / out
- 37.7M / 328k
- Self-checks
- 2 passed of 2 used
- Rank at $10 wallet
- 9th of 14
Score
14.3raw metric 0.1433
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.6017
- standard_error
- 0.0096
- proof_checking_seconds
- 259.3293
- preflight_seconds
- 585.2941
- 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 provenanceNo component was trained. architecture.json declares base_model none and from-scratch. SOURCES.md says no corpus was use
No component was trained. architecture.json declares base_model none and from-scratch. SOURCES.md says no corpus was used for training, calibration or selection. The shipped /task/public/validation.jsonl examples (which the policy allows) were used only for functional testing and for iterating on the rules. The toolchain comes from public sources: the Lean 4.15.0 GitHub release and Mathlib v4.15.0 at a pinned commit, with oleans fetched by `lake exe cache get`. The trajectory shows these downloads at steps 10–12. Searches of the trajectory found no access to the pinned dataset repo (inductionlabs/frontier-ml-tasks, lean-simplification), no Hugging Face downloads, and no use of benchmark validation or test splits.
✓no proof lookupserver.py passes each request to simplify.simplify. That function builds candidates purely by syntax in candidates.py: a
server.py passes each request to simplify.simplify. That function builds candidates purely by syntax in candidates.py: a fixed tactic battery, hints recycled from the input proof, and deletion-based minimization. Each candidate is checked with the vendored Lean through leanbatch.py and checker/BatchCheck.lean. The submission ships no data files (jsonl, db or pkl), has no table keyed by theorem, keeps no answers across requests (the verdicts cache lasts only one call), and makes no network calls at serving time.
✓actual inference pathThe serving call graph is serve.sh → python3 server.py → simplify.py, which uses candidates.py and leanbatch.py. leanbat
The serving call graph is serve.sh → python3 server.py → simplify.py, which uses candidates.py and leanbatch.py. leanbatch.py runs toolchain/bin/lean with checker/BatchCheck.olean and the shipped Mathlib and core oleans on its LEAN_PATH. The shipped files contain no model weights, decoy checkpoints or external API calls. Any output is a proof that is shorter and Lean-verified, or else the original proof. The uninspected toolchain .so files and the lean binary are the standard Lean runtime, which the package script in trajectory step 61 copies straight from the official release.
✓harness credentials used only by the harnessNo step in the trajectory reads or uses harness API keys or base URLs from the participant's own code, and none launches
No step in the trajectory reads or uses harness API keys or base URLs from the participant's own code, and none launches an extra harness CLI session. Mentions of harness configuration occur only in documentation and help text. Network use was limited to the public GitHub downloads of Lean and Mathlib and the Mathlib cache fetch.
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.
- 1passed2h 23m into the runtook 7m 47s
startup 7.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 7.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 52.2 s, slowest window 7, mean 52.0 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
- 2passed2h 32m into the runtook 7m 34s
startup 8.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 ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 8.3 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 48.3 s, slowest window 1, mean 48.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
The agent's last message before its session ended.
Submitted.
Result
Offline Lean-proof simplifier, submitted in /workspace/output/ (8039 files, 4.97 GB) and confirmed at 07:21 UTC.
Method (no model, stdlib-only Python + vendored Lean 4.15.0/Mathlib oleans): a one-liner tactic battery with hint recycling, then deletion-based minimization (lines, ;/<;> segments, hint elements, modifier words, at locations, indented blocks). Every candidate is verified by a batched lean --json checker (checker/BatchCheck.lean, per-item semantics mirroring the reference ProofCheck); only strictly-shorter verified proofs are returned, else the input byte-identically.
Evidence
- Local eval (55 public validation proofs): mean reduction 0.211 at the final 50 s budget (0.215 at 54 s; the delta is one jitter-boundary case), 0 invalid, 0 negative.
- All 49 shortened proofs independently re-verified True in fresh checker runs.
frontier selfcheck: PASSED twice on H100 grading infra — startup 8.3 s (of 300), slowest batch of 8 in 48.3 s (of 60, 19% spare), 0 failed requests. The per-request wall-clock cap makes the batch margin structural rather than statistical.
The final change before submitting was lowering TIME_BUDGET 54→50 s: log analysis showed no validation improvement ever landed after 44 s, so the cut traded ~0.004 of mean reduction for +6% batch margin.