Submit

1. Put your proof somewhere the lean-eval CI can fetch it

Accepted submission sources are URLs of one of these shapes:

• a GitHub repository: https://github.com/<owner>/<repo>

• a GitHub repository pinned to a branch, tag, or commit: https://github.com/<owner>/<repo>/tree/<ref> or https://github.com/<owner>/<repo>/commit/<sha>

• a public gist: https://gist.github.com/<user>/<gist-id> (optionally with a revision suffix)

Private GitHub repositories are supported. To use one, install the lean-eval-bot GitHub App on the repository first, so that the CI can clone it.

Secret (unlisted) gists are not supported in v1. Make your gist public, or host the proof in a repository.

2. Lay out the proof so CI can find it

The CI walks whatever you submit 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

• a gist containing a two-file minimum: a lakefile.toml with name = "<problem_id>" and a Submission.lean

For each matched directory the CI 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.

3. Open a submission issue

Click Submit benchmark solution to open a pre-filled issue. The form asks for:

• a submission URL in one of the shapes above

• a free-form model identifier that identifies the model or system that produced the proof

• whether the exact solutions are public, planned for publication, or private with no current publication plan

• an actual or intended publication date in YYYY-MM-DD format when applicable

You can also provide an optional description of how the solution was produced.

When you submit the issue, the lean-eval CI takes over. It clones your content, scans for benchmark workspaces, runs comparator on every match, and records any newly-solved problems in the leaderboard repository. The CI comments on your issue with a per-problem pass/fail summary and closes it when done. Any problem that passes is added to your results/<your-github-login>.json record.

Submissions are cumulative. Every success is sticky, and there is no limit on how many times you can submit. Resubmit whenever you have new proofs.

What becomes public

Only the information you enter on the submission form, plus the list of problems your submission solved, becomes public. Your proof is never copied out of the ephemeral workflow runner into any public artifact. The public results store records submission provenance, timestamps, and your submission-time publication declaration.

If your submission source was a public repository or a public gist, the leaderboard may link to it so that others can inspect your solution. If the source was private, no link is published.

LeanEval supports open science and does not prohibit publishing exact solutions. Making solutions public can help library development and let others study and build on your work. However, it also lets solutions be copied directly and may cause them to enter future model-training data, reducing our ability to treat those problems as unseen evaluation data.

Please consider these tradeoffs when deciding whether and when to publish. You can freely publish methods, tooling, prompts, aggregate results, and reusable library contributions without publishing the exact benchmark solutions. There is no required embargo: the decision remains yours.

The intended date requested for planned publication is your current best estimate. It records your intention when you submit and is not a commitment.