# Solver templates & Lean problems

Manage your private Playground Lean 4 solver snippets and custom problems for `solver-participation` competitions. Solver templates can be copied into a [Playground run](./playground.md#submit-a-run) and submitted to a competition.

You only see and modify resources owned by the calling account.

Use track IDs from the target competition's `submissionSpec.catalog.tracks[].id`; for the Stage 2 Lean competition, the track IDs are `solo` and `marathon`.

## List solver templates

```http
GET /api/public/v1/solver-templates
```

**Scope**: `playground.read`. This endpoint is cursor-paginated.

Lists solver templates owned by the calling account. The list view omits `solverCode`; call [Get a solver template](#get-a-solver-template) for the body.

### Query parameters

| Parameter | Type    | Required | Description                                   |
| :-------- | :------ | :------: | :-------------------------------------------- |
| `track`   | string  | No       | Track ID filter, such as `solo` or `marathon`. |
| `cursor`  | string  | No       | Opaque cursor from the previous `nextCursor`. |
| `limit`   | integer | No       | Page size. Default `25`, maximum `100`.       |

### Response fields

| Field        | Type          | Description                                  |
| :----------- | :------------ | :------------------------------------------- |
| `items[]`    | [SolverTemplateSummary](#solver-template-summary-fields)[] | Solver template records without `solverCode`. |
| `nextCursor` | string \| null | Cursor for the next page, or `null`.         |

### Solver template summary fields

| Field                               | Type           | Description                                                    |
| :---------------------------------- | :------------- | :------------------------------------------------------------- |
| `id`                                | string         | Solver template ID.                                            |
| `title`                             | string         | Template title.                                                |
| `track`                             | string         | Track ID, such as `solo` or `marathon`.                        |
| `sourceContributorNetworkItemId`    | string \| null | Contributor Network item this template was forked from.        |
| `publishedContributorNetworkItemId` | string \| null | Active Contributor Network item published from this template.  |
| `createdAt`                         | string         | ISO 8601 UTC creation timestamp.                               |
| `updatedAt`                         | string         | ISO 8601 UTC update timestamp.                                 |

### Solver template fields

`SolverTemplate` includes all [SolverTemplateSummary](#solver-template-summary-fields) fields plus:

| Field        | Type   | Description    |
| :----------- | :----- | :------------- |
| `solverCode` | string | Lean 4 source. |

```json
{
  "ok": true,
  "data": {
    "items": [
      {
        "id": "sst_01HXYZ...",
        "title": "Nat induction starter",
        "track": "solo",
        "sourceContributorNetworkItemId": null,
        "publishedContributorNetworkItemId": null,
        "createdAt": "2026-04-12T08:21:30Z",
        "updatedAt": "2026-05-04T17:02:11Z"
      }
    ],
    "nextCursor": null
  }
}
```

## Get a solver template

```http
GET /api/public/v1/solver-templates/{templateId}
```

**Scope**: `playground.read`.

Returns one solver template, including `solverCode`.

### Path parameters

| Parameter    | Type   | Required | Description         |
| :----------- | :----- | :------: | :------------------ |
| `templateId` | string | Yes      | Solver template ID. |

### Response fields

Returns a [SolverTemplate](#solver-template-fields), including `solverCode`.

## Create a solver template

```http
POST /api/public/v1/solver-templates
```

**Scope**: `playground.write`.

Creates a solver template owned by the calling account.

### Request fields

| Field                            | Type   | Required | Description                                              |
| :------------------------------- | :----- | :------: | :------------------------------------------------------- |
| `title`                          | string | Yes      | Template title.                                          |
| `solverCode`                     | string | Yes      | Lean 4 source.                                           |
| `track`                          | string | No       | Track ID, such as `solo` or `marathon`. Default `solo`.  |
| `sourceContributorNetworkItemId` | string | No       | Contributor Network item this template was forked from.  |

```json
{
  "title": "Nat induction starter",
  "solverCode": "theorem starter : ... := by ...",
  "track": "solo",
  "sourceContributorNetworkItemId": "cn_01HX0PA..."
}
```

### Response fields

Returns the created [SolverTemplate](#solver-template-fields), including `solverCode`.

## Update a solver template

```http
PATCH /api/public/v1/solver-templates/{templateId}
```

**Scope**: `playground.write`.

Partially updates a solver template. Provide at least one request field. `track` and `sourceContributorNetworkItemId` are fixed after creation. A template published on the Contributor Network is read-only; withdraw the published item first.

### Path parameters

| Parameter    | Type   | Required | Description         |
| :----------- | :----- | :------: | :------------------ |
| `templateId` | string | Yes      | Solver template ID. |

### Request fields

| Field        | Type   | Required | Description       |
| :----------- | :----- | :------: | :---------------- |
| `title`      | string | No       | New title.        |
| `solverCode` | string | No       | New Lean 4 source. |

### Response fields

Returns the updated [SolverTemplate](#solver-template-fields), including `solverCode`.

## Delete a solver template

```http
DELETE /api/public/v1/solver-templates/{templateId}
```

**Scope**: `playground.write`.

Deletes a solver template owned by the calling account. A template published on the Contributor Network is read-only; withdraw the published item first.

### Path parameters

| Parameter    | Type   | Required | Description         |
| :----------- | :----- | :------: | :------------------ |
| `templateId` | string | Yes      | Solver template ID. |

### Response

Returns `204` with no body.

## List custom problems

```http
GET /api/public/v1/lean-problems
```

**Scope**: `playground.read`. This endpoint is cursor-paginated.

Lists private Lean statement pairs owned by the calling account.

### Query parameters

| Parameter | Type    | Required | Description                                   |
| :-------- | :------ | :------: | :-------------------------------------------- |
| `cursor`  | string  | No       | Opaque cursor from the previous `nextCursor`. |
| `limit`   | integer | No       | Page size. Default `25`, maximum `100`.       |

### Response fields

| Field        | Type          | Description                          |
| :----------- | :------------ | :----------------------------------- |
| `items[]`    | [CustomProblem](#custom-problem-fields)[] | Custom problem records.              |
| `nextCursor` | string \| null | Cursor for the next page, or `null`. |

### Custom problem fields

| Field       | Type    | Description                                  |
| :---------- | :------ | :------------------------------------------- |
| `id`        | string  | Problem ID to send in `problemIds`.          |
| `lhsName`   | string  | Name of the left-side Lean declaration.      |
| `lhsText`   | string  | Left-side Lean source.                       |
| `rhsName`   | string  | Name of the right-side Lean declaration.     |
| `rhsText`   | string  | Right-side Lean source.                      |
| `isCustom`  | boolean | Always `true` for this endpoint.             |

## Get a custom problem

```http
GET /api/public/v1/lean-problems/{problemId}
```

**Scope**: `playground.read`.

Returns one [CustomProblem](#custom-problem-fields) owned by the calling account.

### Path parameters

| Parameter   | Type   | Required | Description        |
| :---------- | :----- | :------: | :----------------- |
| `problemId` | string | Yes      | Custom problem ID. |

### Response fields

Returns a [CustomProblem](#custom-problem-fields).

## Create a custom problem

```http
POST /api/public/v1/lean-problems
```

**Scope**: `playground.write`.

Creates an immutable private Lean statement pair.

### Request fields

| Field     | Type   | Required | Description                                         |
| :-------- | :----- | :------: | :-------------------------------------------------- |
| `lhsName` | string | No       | Name of the left-side declaration. Derived if omitted. |
| `lhsText` | string | Yes      | Left-side Lean source.                              |
| `rhsName` | string | No       | Name of the right-side declaration. Derived if omitted. |
| `rhsText` | string | Yes      | Right-side Lean source.                             |

```json
{
  "lhsName": "my_lemma",
  "lhsText": "theorem my_lemma : ... := by ...",
  "rhsName": "my_lemma_alt",
  "rhsText": "theorem my_lemma_alt : ... := by ..."
}
```

### Response fields

Returns the created [CustomProblem](#custom-problem-fields).

## Delete a custom problem

```http
DELETE /api/public/v1/lean-problems/{problemId}
```

**Scope**: `playground.write`.

Deletes a custom problem owned by the calling account. Existing runs that referenced the problem keep their stored copy and history.

### Path parameters

| Parameter   | Type   | Required | Description        |
| :---------- | :----- | :------: | :----------------- |
| `problemId` | string | Yes      | Custom problem ID. |

### Response

Returns `204` with no body.

## Errors

See [Errors](../errors.md). Endpoint-specific:

| Code                     | HTTP | When                                                       |
| :----------------------- | :--: | :--------------------------------------------------------- |
| `SOLVER_TEMPLATE_LOCKED` | 403  | Solver template is published. Withdraw it first. |
| `LEAN_SOURCE_INVALID`    | 422  | `solverCode` or custom-problem text failed the Lean 4 parser. |