Submit

1. Prepare a source LeanEval can fetch

Authenticated submissions require a 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. Choose the source and identify the model or system that produced the proof. The application walks the submitted source and tries 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 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.

3. Confirm the release terms

The authenticated submission action includes 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 and publish evaluation metadata and results. I will not submit secrets or material I am not authorized to disclose. If I choose scheduled release, I also confirm that I have authority to license the accepted source under the Apache License 2.0 and authorize Lean Eval to publish it two UTC calendar months after acceptance.

Scheduled release is recommended and selected by default. You may instead choose to keep accepted source 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.

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.