Submit

1. Prepare a source LeanEval can fetch

Authenticated submissions accept a public or private GitHub repository in owner/repository form and the exact 40-character source commit to evaluate. Before submitting, install both read-only GitHub Apps on that one repository:

• Lean Eval Source Reader, so authenticated intake can verify the repository and exact commit

• lean-eval-bot, so the archive and evaluation workflow can clone that same immutable commit

2. Submit through the authenticated application

Continue to the secure submission service and sign in with GitHub. Enter one problem id, choose the exact source, and identify the model or system that produced the proof. LeanEval resolves the problem group and current statement revision from the protected catalog. Formalization problems must be visible and active; software-verification problems may be visible and draft or active.

The source may be:

• a clone of a single generated workspace from leanprover/lean-eval/generated/

• a fork of leanprover/lean-eval itself with your proofs under the relevant generated/<problem_id>/ directories

• a custom repository containing several benchmark workspaces side by side

LeanEval evaluates only the selected problem. For its matching directory, LeanEval overlays only your Submission.lean and any files under Submission/**/*.lean onto a pristine copy of the benchmark's workspace for that problem. Every other file in your submission is ignored, including Solution.lean, Challenge.lean, or any modified lakefile.toml. The CI then runs comparator to check the proof.

Before evaluation, LeanEval records the exact source revision and digest and stores a private encrypted archive bound to that submission. Submission source and credentials are not exposed through public workflow artifacts or logs. An exact resubmission by the same owner returns the original receipt instead of starting duplicate work. Each owner may have at most four active submissions.

3. Confirm the release terms

The authenticated submission action requires you to confirm all of the following:

• you are authorized to submit the exact source and metadata

• LeanEval may privately fetch, archive, build, and execute the exact commit

• the encrypted archive may be retained indefinitely, including when evaluation rejects or fails

• the result and submitted metadata may be displayed publicly, and the submission contains no secrets

• if scheduled, accepted source will be published under Apache License 2.0 exactly two UTC calendar months after acceptance

• if initially withheld, later scheduling is irreversible

Scheduled release is recommended and selected by default. You may instead choose to keep accepted source from a private repository private; the public result remains visible with its solution marked as withheld. If the initial choice is private, you may later authorize scheduled release with the same license confirmation. That change is irreversible: a scheduled choice cannot be changed back to private. A public repository must use scheduled release.

What becomes public, and when

The following release policy applies to submissions made through the authenticated application. Submissions through the fallback issue-intake path retain their existing policy.

Submission metadata and evaluation results may become public when the result is recorded. Private source remains in the encrypted archive during the release delay.

If you choose scheduled release, LeanEval automatically publishes the exact accepted Submission.lean and files under Submission/ under the Apache License 2.0 two UTC calendar months after acceptance. Repository metadata, credentials, challenge files, modified build files, and unrelated source files are not included in that release.

Only schedule files that you have authority to provide and license. Do not include secrets. If you choose to keep accepted source private, the public leaderboard keeps the evaluation result but shows that the solution is withheld. You may later schedule release; that transition is irreversible, and scheduled release cannot later be changed to private.