# Mathematics Distillation Stage 2 Playground

Competition ID: `mathematics-distillation-challenge-equational-theories-stage2`

Use this guide when automating Lean solver practice runs for Mathematics Distillation Stage 2.

## Endpoint map

Use `competitionId = mathematics-distillation-challenge-equational-theories-stage2`.

| Task | Endpoint | Scope |
| :--- | :--- | :--- |
| Read accepted models | `GET /api/public/v1/competitions/{competitionId}/playground/models` | `playground.read` |
| Read problem sets | `GET /api/public/v1/competitions/{competitionId}/playground/problem-sets` | `playground.read` |
| Read a problem set | `GET /api/public/v1/competitions/{competitionId}/playground/problem-sets/{problemSetId}` | `playground.read` |
| Create a practice run | `POST /api/public/v1/competitions/{competitionId}/playground/runs` | `playground.write` |
| Read runs, results, and events | Shared Playground run endpoints | `playground.read` |

Supporting resources:

- Manage reusable solver code and custom Lean problems with the [Solver templates](../solver-templates.md) endpoints.
- Publish or browse shared solver templates with the [Contributor Network](../contributor-network.md) endpoints.
- Submit the final formal entry with the [Stage 2 competition guide](../competitions/mathematics-distillation-stage2.md).

## Run payload

Stage 2 uses `submissionSpec.kind: "solver-participation"` for formal submissions. Playground runs execute one Lean 4 solver against selected Lean problems.

**Example request body**

```json
{
  "solverCode": "theorem solver : ... := by ...",
  "solverName": "induction-v3",
  "problemIds": ["prob_01HX...", "prob_01HY..."],
  "allowedModels": ["openai-gpt-oss-120b"]
}
```

Payload fields:

- `solverCode` is required. The run stores a copy of the Lean 4 source.
- `solverName` is optional. Use it as a readable run label.
- `problemIds[]` is required. Use problem IDs from problem sets or private custom problems.
- `allowedModels[]` is optional. Use model IDs from the Playground models endpoint.

## Recommended workflow

1. Read `submissionSpec.catalog.tracks[]` and `submissionSpec.catalog.models[]` from the competition detail.
2. Create or update solver code with the [Solver templates](../solver-templates.md) endpoints.
3. Read available Playground models and Lean problem sets.
4. Submit a Playground run for the candidate solver.
5. Read run results and iterate on the solver source.
6. Submit the final `track`, `modelId`, and `solverCode` through the Stage 2 competition submission endpoint.

See [Playground](../playground.md) for the shared endpoint field tables.