# List Playground examples

```http
GET /api/public/v1/competitions/lean-kernel-challenge/playground/examples
```

**Scope**: none. No authentication is required.

Returns the current published catalog of read-only official example sources. Every example is a complete `Submission.lean` for one Problem.

Use an official example as a starting point for an editable Solution, then create a practice Run to evaluate your changes.

## Query parameters

| Parameter | Type, requirement, and meaning |
| :--- | :--- |
| `problem` | **Optional string.** Exact, case-sensitive `problemId` returned by [List problems](./list-problems.md). Omit it to return the complete catalog. An unmatched value returns an empty `items` array. |

The endpoint returns examples for both `available` and `unavailable` Problems because availability only controls creation of new work.

## Catalog behavior

- `items` uses a deterministic server-defined order. Preserve that order; do not maintain a client-side example list or infer priority from `exampleId` or `name`.
- The complete matching catalog is returned in one response; this bounded collection does not use cursor pagination.
- Reading examples does not save a Solution, create a Run or submission, or consume a Playground quota.
- The catalog remains readable when the Playground is read-only and does not require enrollment or a Competition Team.

Before public Competition discovery opens, the endpoint returns `404 DISCOVERY_NOT_LAUNCHED`. A hidden or nonexistent Competition returns `404 NOT_FOUND`.

## Response fields

### Data

| Field | Type and meaning |
| :--- | :--- |
| `items` | [`PlaygroundExample[]`](#playgroundexample) — Complete matching official example catalog. |

### `PlaygroundExample`

| Field | Type and meaning |
| :--- | :--- |
| `exampleId` | `string` — Opaque example identifier. Do not parse or construct it. |
| `problemId` | `string` — Exact current Problem ID to which the example belongs. |
| `name` | `string` — Participant-facing example name. It is not a user Solution name. |
| `filename` | `"Submission.lean"` — Exact root filename of the single-file source. |
| `content` | `string` — Complete, non-empty UTF-8 source of `filename`, including its final newline when present. |

## Example request

```bash
export SAIR_API_BASE="https://api.sair.foundation/api/public/v1"
export SAIR_PROBLEM_ID="fib"

curl \
  "$SAIR_API_BASE/competitions/lean-kernel-challenge/playground/examples?problem=$SAIR_PROBLEM_ID"
```

## Example response

The identifier below is illustrative. The returned source is complete.

```json
{
  "ok": true,
  "data": {
    "items": [
      {
        "exampleId": "fib-baseline",
        "problemId": "fib",
        "name": "baseline",
        "filename": "Submission.lean",
        "content": "import Spec\n\nnamespace Submission\n\ndef impl : Nat → Nat := fibSpec\n\ntheorem impl_correct : ∀ n, impl n = fibSpec n := fun _ => rfl\n\nend Submission\n"
      }
    ]
  }
}
```

Successful responses use `Content-Type: application/json`.

## Create an editable copy

The returned source is immutable and cannot be run, renamed, edited, shared, or submitted directly. To start from it, explicitly create a private [saved Solution](./save-playground-solution.md) with `content` as `files["Submission.lean"]`. The new Solution is an independent user-owned copy; later catalog changes do not rewrite it.

Creating that copy is a separate authenticated write. It must satisfy the current Playground lifecycle, enrollment, Problem, naming, Workspace, and concurrency rules. Saving does not create a Run, formal submission, or Contributor Network publication.

## Errors

| HTTP | Code | When |
| :---: | :--- | :--- |
| `404` | `DISCOVERY_NOT_LAUNCHED` | Lean Kernel public discovery is not open. |
| `404` | `NOT_FOUND` | The Competition does not exist or is not publicly visible. |
| `502` | `PLATFORM_UNAVAILABLE` | Competition visibility cannot be verified. |

See [Errors](../../../errors.md) for the standard error envelope and shared request rules.