Submit

Server intake prelaunch — not accepting submissions

Production server intake is disabled. Submit now through the GitHub issue form with your Submission.lean source; the existing workflow verifies each matching proof with comparator before recording an accepted result.

Production server intake is not enabled. The authenticated application at lean-eval-submission-server.lean-eval.workers.dev is visible for prelaunch review, but it is not accepting submissions.

To submit now, use the legacy GitHub issue form in leanprover/lean-eval-submissions. It remains the current functioning submission path until production server intake launches. You can then return to the leaderboard.

After launch, GitHub OAuth callbacks and the application session will be scoped to the separate Worker origin that handles private intake.

1. Submit through the current GitHub issue intake

Open the legacy GitHub issue form and follow its current source and metadata instructions. Do not use the prelaunch Worker application to submit a solution while server intake is disabled.

2. Preview the planned authenticated workflow

The secure submission service is in prelaunch and is not accepting submissions. When production intake launches, it will require a private GitHub repository in owner/repository form and the exact 40-character source commit to evaluate. Submitters will first install the Lean Eval Source Reader GitHub App on that repository, then sign in with GitHub, choose the source, and identify the model or system that produced the proof.

The application will walk the submitted source and try every directory containing a lakefile.toml whose name field matches a benchmark problem id, and which has a Submission.lean next to it. For example:

  • 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

For each matched directory LeanEval will overlay 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 will be ignored, including Solution.lean, Challenge.lean, or any modified lakefile.toml. The CI will then run comparator to check the proof.

Before evaluation, LeanEval will record the exact source revision and digest and store a private encrypted archive bound to that submission. Submission source and credentials will not be exposed through public workflow artifacts or logs.

3. Confirm the release terms

When production server intake launches, the submission action will include this acknowledgement:

By submitting, I confirm that I have authority to provide this source. I authorize Lean Eval to store and run it privately for evaluation, publish evaluation metadata and results, and, two UTC calendar months after acceptance, publish the submitted source under the Apache License 2.0. I will not submit secrets or material I am not authorized to disclose.

Source accepted through that application will be scheduled for publication by default. Submitters may opt out at any time before release, either in the application or by asking later. The public result then remains visible with its solution marked as withheld.

What becomes public, and when

The following release policy applies to submissions made through the authenticated application after production intake launches. Current issue intake retains its 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.

Unless you opt out, 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 submit files that you have authority to provide and license. Do not include secrets. If you opt out before release, the public leaderboard keeps the evaluation result but shows that the solution is withheld.