lean-eval-submissions

The submission pipeline and the stored results for the lean-eval benchmark.

This repository owns two things:

• The submission process — the issue intake, the submission workflow that fetches a submission, evaluates it with comparator, and records the outcome, and the reconciler that catches stranded submission issues.
• The results store — results/<github-login>.json, the append-only public log of solved problems.

The benchmark problem set, the lean-eval CLI, and the comparator/landrun security model live in leanprover/lean-eval. The public leaderboard that renders these results is leanprover/lean-eval-leaderboard (view it →).

Submitting a solution

The preferred submission path is the LeanEval submission service.

Before submitting through the service, install both read-only Apps on only the repository you intend to submit:

• LeanEval Source Reader verifies the repository and exact source commit during intake.
• lean-eval-bot lets the archive and evaluation workflow fetch that same commit.

The service verifies both installations and exact-commit access before it records or dispatches a submission. This is enforced for browser and headless submission clients; it is not a form checkbox or user assertion.

The service accepts a problem ID, declared model, exact repository and commit, publication choice, production metadata, and acceptance of the current terms. It resolves the problem group and current statement revision itself from the protected LeanEval catalog. Formalization problems must be visible and active; software-verification problems may be visible and draft or active. Clients do not supply either canonical field.

Scheduled publication is the recommended default. A public repository must use scheduled publication. A private repository may instead keep accepted source private and irreversibly schedule it later. Accepted scheduled source is released under Apache License 2.0 exactly two UTC calendar months after acceptance.

Submitting the same owner, repository, commit, problem, and resolved statement revision again returns the original submission instead of dispatching duplicate work. An owner may have at most four active submissions; completed and terminal submissions, and incomplete submissions older than 24 hours, do not occupy a slot.

GitHub issue intake remains available during the transition and is provisionally scheduled to close no earlier than 2026-09-30T06:57:10Z. Closure is not automatic: issue intake will remain open if a severity-high incident is unresolved or the adoption, service-stability, or final historical cutoff and append-only delta gates have not passed. Any closure will be confirmed separately.

While issue intake remains open, you can use the Submit benchmark solution form. Point it at any content that contains at least one lakefile.toml whose name matches a benchmark problem id with a Submission.lean alongside it — a generated workspace, a fork of leanprover/lean-eval with changes under generated/, a repo with several workspaces, or a public gist. The CI walks the content and tries every match.

The legacy issue workflow discovers every matching workspace. In contrast, the submission service evaluates only the exact problem selected in the request. The exact repository snapshot is privately fetched, archived, built, and executed. It is not published before the selected release time; only results and submitted metadata are public during the embargo or when source is withheld. Do not include secrets in a submitted repository or its metadata.

If you use the legacy issue path and your submission lives in a private repository, install the lean-eval-bot GitHub App on it so the CI can clone it: https://github.com/apps/lean-eval-bot.

Headless service contract

Headless clients first request a source-bound challenge from POST /api/v1/agent/challenges, prove control through the returned exact tag and secret Gist, and then send that signed challenge to POST /api/v1/agent/submissions. The submission object has this closed v2 shape:

{
  "schema_version": 2,
  "problem_id": "two_plus_two",
  "declared_model": "Example Model",
  "source_repository": "owner/repository",
  "source_commit": "0123456789abcdef0123456789abcdef01234567",
  "publication_choice": "scheduled",
  "production_metadata": {},
  "terms_version": "lean-eval-intake-terms-v1",
  "terms_accepted": true
}

Unknown fields and older schema versions are rejected. The server returns the canonical problem group and statement revision in the receipt.

Legacy issue submission through the GitHub API

API-created issues are supported. Create an issue whose title starts with [submission] and whose body uses the same rendered Markdown sections as the submission Issue Form. For example, gh issue create --repo leanprover/lean-eval-submissions --title '[submission] my proof' --body-file submission.md uses the GitHub API.

The body must include the required Submission URL, Model, exact-solution publication fields, and all three checked acknowledgements. Do not depend on the API request's labels field: GitHub drops labels requested by issue authors without triage permission. The intake workflow validates a complete submission body, applies the submission label, and starts evaluation.

Legacy issue publication metadata

LeanEval supports open science and does not prohibit publishing exact solutions. Public solutions can help library development and let others study and build on the work. They can also be copied directly or enter future model-training data, reducing our ability to treat those problems as unseen evaluation data.

The submission form asks you to choose one of three statuses:

• Public, with the actual publication date in YYYY-MM-DD format.
• Private, but publication is planned, with your current best estimate of the intended publication date in YYYY-MM-DD format. This is a submission-time snapshot, not a commitment.
• Private, with no current publication plan.

These three choices apply only to the temporary legacy issue form. New service submissions use the scheduled-or-withheld policy above. There is no required embargo for legacy issue submissions. Please consider the tradeoffs when deciding whether and when to publish. Methods, tooling, prompts, aggregate results, and reusable library contributions can be published without publishing the exact benchmark solutions.

Audit archive

Every service submission's compressed source tarball is retained indefinitely, including submissions that reject or fail. Each archive uses a fresh data key and a schema-version-3 per-submission key envelope. The encrypted archives live in the private leanprover/lean-eval-audit repository so that the exact bytes evaluated for any past submission remain recoverable if a comparator regression, soundness incident, or research question requires re-examining them. Archive-key wrapping and release unwrapping use separate, least-privilege AWS roles. Submitting explicitly agrees to this retention and to private fetch, archive, build, and execution before State accepts the request.

The compressed source tarball is capped at 100 MB; submissions above the cap are rejected before evaluation. See docs/audit-archive.md for the design and the decryption procedure.

Results store

results/ holds machine-written artifacts produced by the submission CI. Do not edit them by hand.

results/
  <github-login>.json

One file per submitter; filenames use the lowercased GitHub login. Users without a successful submission have no file.

Successes are sticky: once a (user, declared model, problem, statement revision) tuple is recorded it is never modified or removed, even if a later submission from the same user no longer proves it.

Results record schema version 2

{
  "schema_version": 2,
  "user": "kim-em",
  "results": [
    {
      "result_id": "r2_...",
      "problem_id": "two_plus_two",
      "statement_revision": 1,
      "declared_model": "Claude Opus 4.7",
      "accepted_at": "2026-05-01T03:16:18Z",
      "benchmark_commit": "953d54a7af5038566775507761e48e365e7feb3b",
      "intake": {"kind": "issue", "issue_number": 45},
      "submission": {
        "kind": "gist",
        "repo": "kim-em/22bad2dccd67bcca0df87c01d072ef39",
        "ref": "567b8d1feebbc6ccbb1f8ebb0a7bbcf5e914f135",
        "public": true
      },
      "production_metadata": {}
    }
  ]
}

The exact identifier contract, full field definitions, schema version 1 mapping, language-neutral fixtures, and guarded migration procedure are documented in docs/results-schema-v2.md. Readers accept results schema versions 1 and 2 during migration; every newly changed file is written using schema version 2.

Write semantics

When the submission CI records a successful submission:

1. It reads and validates schema version 1 or 2, or starts an empty schema version 2 array.
2. It computes the stable ID from login, verbatim model, problem, and the statement revision frozen into the evaluation artifact.
3. If that ID exists, it does nothing; otherwise it appends a schema version 2 record.
4. If at least one new record was added, the CI commits and pushes; otherwise it makes no commit.

Breaking schema changes bump schema_version; consumers should refuse a file whose schema_version they do not know.

How the pipeline fits together

submission service
  → verify the exact source and current catalog problem
  → atomically accept append-only State and enqueue dispatch
  → archive the immutable source snapshot with its per-submission envelope
  → evaluate only the accepted problem and record its terminal lifecycle
  → write any accepted immutable Result
  → refresh the lifecycle-aware leaderboard

legacy submission issue (temporary overlap)
  → validate issue metadata and scan matching workspaces
  → archive, evaluate, and append accepted Results

submission-reconciler.yml is an hourly safety net: it closes submission issues that never received a bot comment (workflow disabled, runner died, etc.).

Operator notes

• Secrets, GitHub Apps, and branch protection: docs/ci-secrets.md.
• Security model / threat analysis: SECURITY.md.
• Local-only replay planner and disposable-VM contract: docs/replay-orchestrator.md.
• Source-minimized historical public replay evidence and its read-only token boundary: docs/public-replay-resolution.md.
• Provider-neutral archive-key envelope and single-use capability claims: docs/key-capability-contract.md.
• Trusted provider-neutral archive writer and server-archive workflow: scripts/archive_envelope.py and .github/workflows/server-archive.yml.
• AWS KMS/DynamoDB adapter and linted SAM infrastructure; production archive Wrap is connected, while production replay remains packet-gated under the standing authorization: scripts/aws_key_adapter.py and infrastructure/aws-key-adapter/template.yaml.
• Concise operator walkthrough for the dedicated account: docs/aws-key-adapter-setup.md.
• ci.yml runs the Python test suite, actionlint, the workflow-pin audit, and tests/test_submission_workflow.py (a structural guard on submission.yml's security-critical shape).