# Lean Kernel Challenge

Use this guide for Stage 1, the Kernel Computation Track: discover the live problem catalog, develop and test Lean workspaces, share saved solutions, and submit formal competition entries.

## Endpoint map

**Competition endpoints**

- Discover the contract with [Get competition detail](./lean-kernel-challenge/get-competition-detail.md), [List problems](./lean-kernel-challenge/list-problems.md), [Get a problem](./lean-kernel-challenge/get-problem.md), and [Get submission spec](./lean-kernel-challenge/get-submission-spec.md).
- Submit and review official entries with [Get my participation](./lean-kernel-challenge/get-my-participation.md), [Submit a Lean file](./lean-kernel-challenge/submit-package.md), [List my submissions](./lean-kernel-challenge/list-my-submissions.md), [Download a submission](./lean-kernel-challenge/download-submission.md), [Get leaderboard](./lean-kernel-challenge/get-leaderboard.md), and [Get a leaderboard entry](./lean-kernel-challenge/get-leaderboard-entry.md).

**Playground endpoints**

- Read the [Playground lifecycle](./lean-kernel-challenge/get-playground-lifecycle.md), then start with [List examples](./lean-kernel-challenge/list-playground-examples.md) and [list](./lean-kernel-challenge/list-playground-solutions.md), [save](./lean-kernel-challenge/save-playground-solution.md), or [delete](./lean-kernel-challenge/delete-playground-solution.md) a Solution.
- [Create](./lean-kernel-challenge/create-playground-run.md), [list](./lean-kernel-challenge/list-playground-runs.md), or [inspect](./lean-kernel-challenge/get-playground-run.md) a practice Run, [cancel it while it is still service-confirmed as queued](./lean-kernel-challenge/cancel-playground-run.md), and [download its immutable source snapshot](./lean-kernel-challenge/download-playground-run.md).

**Contributor Network endpoints**

- [List](./lean-kernel-challenge/list-contributor-packages.md) or [get](./lean-kernel-challenge/get-contributor-package.md) shared packages. To publish, [preview an exact saved Solution revision](./lean-kernel-challenge/preview-contributor-publication.md), then [publish the confirmed revision](./lean-kernel-challenge/publish-contributor-package.md). You can also [download](./lean-kernel-challenge/download-contributor-package.md) or [withdraw](./lean-kernel-challenge/withdraw-contributor-package.md) a shared package.

The Playground API evaluates source from a saved Solution. Save the complete Workspace, then create a Run from its exact revision.

## Choose the right resource

| Resource | Source and mutability | Competition effect |
| :--- | :--- | :--- |
| **Solution** | An owner-editable Workspace with a stable ID and increasing revision. It contains `Submission.lean` and may contain compatible auxiliary files under `Submission/`. | None. Saving, editing, or deleting a Solution does not run or submit it. |
| **Run** | An immutable execution snapshot of one exact Solution revision and the runtime contract in effect when the Run is created. | Practice feedback only. A Run never becomes a formal result or leaderboard entry. |
| **Formal submission** | An immutable, team-owned candidate for one Problem. Its JSON request contains the exact text of one `Submission.lean`. | Eligible for the official cutoff selection and later evaluation. |
| **Contributor Network publication** | A preview-confirmed, immutable snapshot of the complete current Solution Workspace. It can be withdrawn, but not edited in place. | None. Publishing does not create a formal submission, score, result, or rank. |

## Competition model

Each released Problem asks for a core Lean implementation `impl` and a proof `impl_correct` that it agrees with that Problem's trusted specification for every input. Problem names, workspaces, rules, and source contracts come from the live catalog and submission spec; clients must not hardcode a catalog revision.

Playground Runs are immediate, non-official evaluations. New Solutions and Runs are accepted only while the Playground is writable. Retained owner-authorized Solutions, Runs, and downloads remain readable when new work is closed.

Formal submissions are accepted during the submission window. At the cutoff, the competition selects the latest valid candidate for each team and Problem. Official results and rankings are organized by Problem and remain private until the corresponding results are published.

Contributor Network publication starts from an exact current Solution revision and includes its complete compatible Workspace. It does not require a successful Run and remains independent of formal submission.

## Formal submission source format

A formal submission contains exactly one non-empty UTF-8 `.lean` source text of at most 1 MiB. Send it as `payload.text` in an `application/json` request; multipart forms and file-reference fields are not supported. The text is stored as:

```text
Submission.lean
```

Read the current byte limit and source contract from [Get submission spec](./lean-kernel-challenge/get-submission-spec.md) immediately before submitting.

A saved Solution is a different resource. Its editable Workspace may contain `Submission.lean` and compatible files under `Submission/`, with up to 256 files and 8 MiB of total source. A Run freezes and evaluates the complete Workspace. Formal submission does not accept a Solution ID, so clients must send the selected root source text explicitly and must not make it depend on auxiliary Workspace files.

The concrete types and specification declaration depend on the Problem. For example, the official `fib` baseline is:

```lean
import Spec

namespace Submission

def impl : Nat → Nat := fibSpec

theorem impl_correct : ∀ n, impl n = fibSpec n := fun _ => rfl

end Submission
```

Open the selected Problem's `officialWorkspace` for its exact declarations. The implementation must be reducible by the Lean kernel. The proof may use only the standard axioms permitted by the official rules; Mathlib, `sorry`, and `native_decide` are not accepted. Follow the rules links returned by the submission spec for the complete contract.

## Recommended workflow

1. [List problems](./lean-kernel-challenge/list-problems.md), select an `available` Problem, and open its `officialWorkspace`.
2. Read the current [submission spec](./lean-kernel-challenge/get-submission-spec.md), then [save a Solution](./lean-kernel-challenge/save-playground-solution.md) from an official example or your own Workspace.
3. Create [practice Runs](./lean-kernel-challenge/create-playground-run.md) from exact saved revisions. Generate one `idempotencyKey` for the intended Run and reuse it only when retrying that same request.
4. To share the Solution, [preview its exact current revision](./lean-kernel-challenge/preview-contributor-publication.md). Confirm the complete Workspace and returned manifest, then [publish the saved revision](./lean-kernel-challenge/publish-contributor-package.md) with a new idempotency key. A Run is not required.
5. Check [your participation](./lean-kernel-challenge/get-my-participation.md). During the submission window, pass through the current opaque `contractVersion` and [submit the formal Lean text](./lean-kernel-challenge/submit-package.md) with a new `idempotencyKey`.
6. Use [submission history](./lean-kernel-challenge/list-my-submissions.md) to verify the stored candidate. Read results and the [per-Problem leaderboard](./lean-kernel-challenge/get-leaderboard.md) after publication.

For every state-changing request that requires an idempotency key, create the key once for one logical action and reuse it after a timeout or uncertain response. If the payload changes, use a new key.

## Responses and errors

JSON responses use the shared [response envelope](../../conventions.md#envelope). Download endpoints return source or package bytes directly.

Each operation page documents its complete request-specific error table. In particular, write operations can reject an unavailable Problem, a closed lifecycle, a stale Solution revision, an outdated contract acknowledgement, or an idempotency key reused with different input. Handle the returned code instead of inferring the cause from HTTP status alone.