Training data and task API

Use the reviewed public curriculum for training or development. Do not call it an unseen test. Full ecosystem and environment contract.

1. Choose what your agent can see

Agent task packages

One instruction, exact prompt, environment contract and response template per task. No reference answers or expert source anchors in this ZIP.

Download prompt-only tasks

Reviewed training pairs

Original reference formula proofs or aligned Lean references, in messages-format JSONL. These contain answers; keep them away from evaluation prompts.

Download training pairs

2. Keep identities and environments fixed

Read task-index.json. Select by track, domain or level, then fetch the linked prompt.json and task.json. Each keeps the original family, public-dev split and content binding; the environment records Lean 4.33.0, Mathlib manifest and evaluator source hashes.

python tools/sog_bench.py check
python tools/sog_bench.py export --output .astis/my-bench-export

Instructions and environment/verifier contracts are separate. No Terminal-Bench task content is imported; this site is not a hosted agent runner.

3. Run graph tasks in Harbor

Optional native tasks use a separate JSON verifier, a digest-pinned Python image and Harbor 0.25.0. The CI runs oracle and empty-answer software fixtures, not models. This does not execute submitted Lean.

Download Harbor operator package Runtime requirements, commands and limitations

Includes oracle answers and verifier material: never give this full ZIP to an agent as closed-book context. Use the prompt-only download above for model inputs. Native runtime acceptance is recorded separately in the CI evidence.

4. Prevent train/test leakage

Paired views and derived variants stay in the same family. All current families are public-dev. Publishing a solution makes it unsuitable as a new unseen test; changing a split label cannot undo exposure.

Record an evaluation run · Rights and restricted-source boundaries · Exact export hashes