# Mathematics Distillation Challenge: Equational Theories - Stage 2

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

Use this guide when automating Stage 2 Lean solver practice, publication, and formal submissions.

## Endpoint map

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

**Competition endpoints**

| Task | Endpoint | Scope |
| :--- | :--- | :--- |
| Read schema | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2`](./api/get-competition.md#mathematics-distillation-stage-2) | `competition.read` |
| Check participation | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/me`](./api/get-my-participation.md#mathematics-distillation-stage-2) | `competition.read` |
| Submit solver | [`POST /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions`](./api/submit.md#mathematics-distillation-stage-2) | `competition.write` |
| Read current submissions across tracks | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions/mine`](./api/list-my-submissions.md#mathematics-distillation-stage-2) | `competition.read` |
| Read one track (legacy) | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions/me?track=solo`](./api/get-my-submission-legacy.md#mathematics-distillation-stage-2) | `competition.read` |
| Read a submission by ID | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions/{submissionId}`](./api/get-submission.md#mathematics-distillation-stage-2) | `competition.read` |
| Download submitted solver source | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions/{submissionId}/download`](./api/download-submission.md#mathematics-distillation-stage-2) | `competition.read` |
| Read leaderboard | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/leaderboard`](./api/get-leaderboard.md#mathematics-distillation-stage-2-example) | `competition.read` |
| Read my standing | [`GET /api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/leaderboard/me`](./api/get-my-standing.md#null-example) | `competition.read` |

**Companion APIs**

- Manage solver templates and custom Lean problems with the [Solver templates](../solver-templates.md) endpoints.
- Run practice jobs with the [Playground](../playground.md) endpoints.
- Publish or browse shared solver templates with the [Contributor Network](../contributor-network.md) endpoints.

## Submission payload

The competition uses `submissionSpec.kind: "solver-participation"`.

**Example request body**

```json
{
  "payload": {
    "track": "solo",
    "modelId": "openai-gpt-oss-120b",
    "solverCode": "theorem solver : ... := by ..."
  },
  "meta": {
    "description": "Marathon-tuned solver.",
    "contributorNetworkItemId": "cn_01HX0PA..."
  }
}
```

Payload fields:

- `payload.track` is required. It must be a track ID from `submissionSpec.catalog.tracks[].id`.
- `payload.modelId` is required. It must be a model ID from `submissionSpec.catalog.models[].id`.
- `payload.solverCode` is required. It is the Lean 4 solver source.
- `meta.description` is optional. Use it for a human-readable note in your own submission history.
- `meta.contributorNetworkItemId` is optional. Use it to record the Contributor Network item this submission references or builds on.

One submission is stored per track. Re-submitting the same track replaces the active entry for that track.

## Recommended workflow

1. Read `submissionSpec.catalog.tracks[]` and `submissionSpec.catalog.models[]` from the competition detail.
2. Create or update reusable solver code with the [Solver templates](../solver-templates.md) endpoints.
3. Use the [Playground](../playground.md) endpoints to run solver practice jobs.
4. Optionally publish useful solver templates through [Contributor Network](../contributor-network.md).
5. Submit the final `track`, `modelId`, and `solverCode` through the competition submission endpoint.
6. Read `/submissions/mine` to confirm current submissions across all tracks, or download one stored solver source by submission ID.

## Submit

```bash
curl -X POST "https://api.sair.foundation/api/public/v1/competitions/mathematics-distillation-challenge-equational-theories-stage2/submissions" \
  -H "Authorization: Bearer $SAIR_API_KEY" \
  -H "Content-Type: application/json" \
  -d '{
    "payload": {
      "track": "solo",
      "modelId": "openai-gpt-oss-120b",
      "solverCode": "theorem solver : ... := by ..."
    },
    "meta": {
      "description": "Playground-tested solver."
    }
  }'
```

See [Competitions](../competitions.md) for the shared endpoint field tables.