PLAN.md

LeanEval overhaul plan

Status: retained product-design reference; superseded for execution. The original RFC was reviewed and merged in lean-eval#536. Written 2026-08-19; execution scope amended 2026-08-25.

Completion amendment, 2026-08-25. The remaining work is governed by the overhaul completion plan and its execution runbook. The completion plan records later maintainer decisions and supersedes conflicting requirements below, in particular Formal Conjectures integration, disproof support, experimental independent kernels, the original phase ordering, and any requirement for a dedicated submission hostname. This file remains the design history and authority for product goals that the completion plan retains.

Terminology: unqualified v1 and v2 refer only to problem sets. This document calls the platform work the lifecycle overhaul, and the resulting system the lifecycle-aware platform. Versioned machine formats are always qualified, for example results schema version 2; their frozen identifiers and filenames may retain strings such as results-v2.

This file retains product details that the completion plan still adopts. It is not an implementation checklist. Current decisions and sequencing live in the completion plan and execution runbook.

This document plans a coordinated overhaul across the LeanEval repositories:

• leanprover/lean-eval, the problem set, generator, and comparator integration;
• leanprover/lean-eval-submissions, the submission pipeline and results store;
• leanprover/lean-eval-leaderboard, the public site at https://lean-lang.org/eval/;
• leanprover/lean-eval-audit (private), the encrypted archive of every evaluated submission.

It also proposes two new repositories (a submission state repo and an extracted generator), and one new service (a submission server).

The Workstreams section records the retained decomposition; current completion state is maintained in the execution runbook.

Relevant retained-product discussion: #Model comparisons for Lean > LeanEval.

Where things stand

The repo currently ships 235 problems, including the 50 AnnalsChallenge statements that landed in lean-eval#532 feat: add 50 AnnalsChallenge problems. Submissions arrive as GitHub issues on lean-eval-submissions, are evaluated by comparator (with nanoda as an independent kernel) in GitHub Actions, and land as sticky (user, model, problem) records in the append-only results store. The leaderboard regenerates from that store daily.

The system works, but it's showing strain:

• Progress has been much faster than expected. Single prompts to frontier models are now clearing previously unsolved problems in about a day, and the question "which problems still resist 24 hours of autonomous work?" is more interesting than raw solve counts.
• We collect almost no data about how solutions were produced, so the leaderboard can't answer the comparison questions people actually ask.
• Historical results need reproducible official-kernel and nanoda replay.
• Solutions leak, get copied, and get resubmitted, and we have no policy or tooling for any of that.
• Metadata mistakes (wrong model name, mis-filed submissions) currently require my manual intervention to fix.
• The leaderboard frontend is failing at scale (Lean macro recursion limits, as the problem count grows).

Goals at a glance

1. Declare a fixed v1 problem set, curated from the current catalog.
2. Replace issue-based intake with a submission server that collects structured metadata and gives submitters self-service tools.
3. Introduce a publication policy for the evaluation groups: submissions are private, and released automatically after two months unless the submitter opts out.
4. Preserve the required official Lean kernel and nanoda checks and replay historical accepted submissions against their exact original pins.
5. Build a replay queue that records terminal official-kernel-plus-nanoda outcomes and computes public per-solution statistics (instruction counts, build cost, size) for accepted submissions, past and future.
6. Rebuild the leaderboard with tabs, unique-solve emphasis, a recent solutions feed, and per-problem comparison pages.
7. Open a software verification problem group, initially all-draft.
8. Add a neutrally named open problems group, which may initially be empty and has no external integration dependency.
9. Launch server intake alongside issue intake for a four-week overlap, then retire issue intake after the notice and stability gates pass.

Each goal gets a section below. The Staging and migration section explains ordering and dependencies.

1. Problem groups and lifecycle

Five properties classify every problem: group, current status, frozen-set membership, visibility, and tags.

Group is the subject-matter dimension, and there are three: formalization evaluation (the current benchmark), software verification, and open problems. Each gets its own leaderboard tab. The open-problems group may be empty initially; eventual content and policy are ordinary LeanEval catalog decisions outside this overhaul.

Current status is orthogonal to group. A problem is draft, active, or archived. Retractions and misformalised statements remain distinguishable from ordinary archival.

• Draft problems are solvable and listed, but outside any frozen set. New problems always enter as draft.
• Active problems belong to the group's current flagship set.
• Archived problems no longer belong to the flagship set. They remain in the repository and keep permanent problem pages.

Frozen-set membership is a separate, immutable relation. A problem may belong to more than one named set. v1 is the first set in the formalization evaluation group; software verification may freeze its own first set later; open problems may freeze a set later through an ordinary LeanEval catalog decision. Publishing a new set does not change any earlier set. Problems selected for the new set become active; other draft problems move to archive, and members of the previous flagship set either join the new set or become archived. In all cases their earlier memberships remain intact.

A problem's group is fixed for its lifetime. Visibility is a further boolean property: the existing test = true manifests and Sandbox examples become hidden problems rather than acquiring another lifecycle status.

Tags are the free dimension: zero or more labels per problem, displayed and filterable, with no effect on policy, standings, or validation. Tags live in the problem manifest (tags = ["annals"]) and are validated by CI against a small registry file (tag name, display label, one-line description), so spelling variants can't drift; adding a tag to the registry is a one-line PR. Tag edits are metadata, freeze-compatible like docstring changes. Topic-area tags (number theory, topology, and so on) are derived automatically from the module path rather than hand-maintained. The first hand-applied tag is annals on the 50 AnnalsChallenge problems, a mechanical backfill.

The leaderboard's site-data schema records group, current status, status history, visibility, tags, and frozen-set memberships. Result records remain immutable. Standings for a named set are computed from its problem membership, so neither a status change nor the publication of a later set rewrites a result.

2. The v1 problem set

Maintainer amendment, 2026-08-21. The original v1 publication selected 118 members under the rule below. The maintainer subsequently authorized ten newly merged problems to be added, producing an effective set of 128. This decision supersedes the statements below that v1 can never receive additions. Existing members still cannot be removed or replaced; the exception is recorded as an append-only, dated amendment with exact PR and merge-commit provenance.

The current catalog grew by accretion. v1 is the first named frozen set in the formalization evaluation group: a curated subset that stays fixed, so that results are comparable over a meaningful window.

Curation. v1 does not exist yet: curation decides what enters it, and once declared, its membership never changes. Nothing is ever removed from a frozen set; if v1 turns out too easy, the correction is a harder v2. An LLM-assisted audit of the full catalog produces a candidate list, which I'll review and decide on. The principles:

• A problem that many people have already solved does not enter v1. Saturated problems tell us nothing.
• A leaked or published solution is evidence against inclusion, but not determinative on its own.
• Known or suspected misformalisation risk excludes a problem until fixed.

Problems not selected for v1. They stay in the repository and keep accepting submissions, but carry archive status and don't count toward v1 standings. Existing solve records are never removed.

Draft. Problems added after the freeze enter draft status: solvable and listed, but outside v1 standings, promoted into v2 or archived at the next release.

Freeze semantics. For problems in v1:

• Set membership is frozen permanently. v2 is a separate set and may overlap v1.
• Statements are frozen. Docstring-only clarifications remain allowed (as in lean-eval#501 and lean-eval#502).
• Toolchain and Mathlib bumps are allowed; statements re-elaborate against the new pins. A bump that changes a statement's meaning is treated as a misformalisation incident.
• New solves continue to enter the v1 standings.

Statement revisions. A frozen-set entry identifies both a problem and its statement revision. Docstring changes do not create a revision. If a frozen statement must change meaningfully, the old revision is marked retracted and the corrected revision returns as draft; existing solves remain attached to the old revision and do not count as solves of the corrected statement. A retracted set entry remains visible in set history but contributes neither a problem nor its solves to current standings. This is the common incident procedure for every group. A logically unchanged source migration may keep the revision only after CI verifies that the generated challenge is unchanged.

Flavour text review. Alongside the audit, a thorough review of the prose attached to every existing problem, bringing it to a uniform standard with three parts:

• an informal statement of the problem;
• citations and literature background;
• hints for solving the problem. These will remain highly variable, and no LLM-generated text goes in the hints.

The freeze permits docstring changes, so this review can run before or after the v1 declaration.

Versioning. Result records already carry benchmark_commit. Frozen-set membership belongs to problems, not results: a solve may count in several sets, including a set declared after the solve was accepted. Statement-changing fixes use the incident procedure above rather than overloading set membership.

I expect v1 to remain the flagship set for at least a couple of months, and to be succeeded only by an equally deliberate v2.

3. The submission server

Issue-based intake has served us, but it can't carry what we now need: structured metadata, post-hoc amendment, self-service repair, and enforcement of the publication policy. The replacement is a small Cloudflare Worker in the style of the Palomar submission server.

Architecture principles:

• The Worker holds no mutable application state between requests. Every durable public fact is an append-only JSON event committed to a new repository (working name: leanprover/lean-eval-state), and every transition is a commit. Source, credentials, and one-time challenges are excluded. Event IDs make retries idempotent, and writers update against the current repository head so two transitions cannot silently overwrite each other. An operator CLI can reconstruct the current view and drive any submission to a terminal state.
• Identity is GitHub. A person signs in with GitHub OAuth so the server can learn the login; the token is checked and discarded, never stored. Private source access uses a read-only GitHub App installation scoped to the submission repository, not a long-lived user token. An agent path (a tag at the submitted commit plus a secret gist owned by the submitting account, carrying an expiring challenge) supports headless submission without a browser. Acceptance of a challenge records its nonce, preventing reuse.
• Evaluation uses an immutable snapshot. At intake, the GitHub App fetches Submission.lean and Submission/ at the declared commit and stores an encrypted snapshot in the audit archive. Evaluation and later release use that snapshot, so neither requires continuing access to the submitter's repository.
• Evaluation stays in GitHub Actions. The server does intake, validation, and record-keeping; comparator runs where it runs today, in public workflows with public logs containing no submission source.
• Base results remain in lean-eval-submissions. Accepted results still land there as immutable records. Amendments, retractions, release events, and replay results live in the state repo. The site-data build materializes the current public view from both repositories; neither event stream is rewritten.

Repository privacy. The audit archive should remain the only private repository. In particular the state repo is designed to be public: submission records, amendments, and queue state aren't confidential (acceptances appear on the leaderboard anyway, and the results store already publishes submission repo names). One-time challenges are signed by the Worker and never committed. Public repositories also keep us on GitHub's free Actions minutes. Every flow that handles embargoed content, including initial evaluation and replay, must ensure that public logs and artifacts contain only verdicts and statistics. Steps that cannot guarantee this run in the private audit repository.

Structured metadata at intake. Replacing today's free-form "how this was produced" box:

• one leaderboard credit identity: the primary model for a single-model run, or an explicit ensemble identity when several models contributed materially;
• component model names and versions, plus orchestrator/harness if any;
• level of human involvement (fully autonomous / human-directed / human-written with AI assistance / other);
• web access during the run (none / search with blocklist / unrestricted / unknown), self-reported;
• compute: wall-clock time, token counts, and estimated cost, with subscription vs API noted;
• the prompt(s) used, optional but encouraged: shared prompts are how techniques spread;
• free-form notes.

All of this is self-reported and displayed as such. We standardize the questions, not the enforcement; see the publication policy section for why I think enforcement of web-access rules isn't realistic for us.

Amendments. The state repo records amendments as first-class, append-only events, authenticated as the GitHub login that owns the base result. A maintainer can handle renamed or deleted accounts, with the intervention recorded publicly.

• Backfill: add the structured metadata above to any of your existing submissions. Backfilled data is permanently marked "backfilled on date", as distinct from "declared at submission", so consumers of the data know which numbers were recorded at the time and which were recalled later.
• Model rename/consolidation: rename or merge model labels within your own account, self-service. The rename history is public on the affected entries; solved_at, benchmark_commit, and submission references are immutable through a rename. Site data maps declared labels to canonical credit identities using a public alias table. Mapping to an existing identity is self-service; a maintainer checks a new identity for duplicates, so spelling variants cannot change unique-solve counts. A merge that collides with an existing (user, model, problem) record preserves both base records but contributes only one solve to standings.
• Repair: correct intake metadata, including the problem ID, only when the immutable comparator record already identifies the corrected challenge. Group follows from the problem and is not independently repairable. A repair cannot turn an evaluation for one challenge into a solve of another.

Deprecation of issue intake. The issue path keeps working through a deprecation window after the server launches (proposal: four weeks), then closes. During the window both paths write the same base-results store, so the site-data build handles them identically. Amendments and the new publication policy are available only through the server path.

4. Publication policy

Today submitters self-declare one of three publication tiers with no enforcement. Two recurring complaints are solution leakage and permanently private solutions. The new policy applies to submissions made through the server. Submissions through the issue path during its deprecation window remain under the old policy because that path does not collect the new acknowledgement.

• Evaluation-group submissions must come from private sources. This applies to the formalization evaluation and software verification groups. (We can't stop simultaneous publication elsewhere, but we ask.) The neutral open-problems catalog launches empty; its eventual source-visibility and submission policy are deferred to a later LeanEval catalog decision.
• Solutions are released automatically two months after acceptance, published by us from the accepted snapshot in the audit archive. Publication contains the exact evaluated Submission.lean and Submission/ files, plus public metadata; it excludes repository metadata, credentials, generated challenge files, and unrelated files. Submitting includes an acknowledgement that the submitter has authority to license those files and grants a license (proposal: Apache 2.0) that takes effect at release.
• Submitters choose scheduled release or private source at submission. Scheduled release is the default and is irreversible. A submitter who chose private source may later authorize scheduled release; the reverse transition is not supported. The current choice is recorded and displayed on the leaderboard entry.
• Existing submissions are grandfathered. Their declared tiers stand. The backfill mechanism includes an invitation to schedule release.

The proposed two-month delay should outlast most evaluation runs while releasing proofs soon enough to remain useful. I'm open to argument about the duration. Before result recording, the recorded choice determines whether the result and release schedule are created together. After result recording, a private-to-scheduled transition atomically records the publication change and creates the missing release schedule. Its eligibility date remains exactly two UTC calendar months after acceptance, so a later authorization may make the release immediately due. Release jobs are idempotent, record failures, and retry without changing the scheduled date.

Audit-archive key management. The archive is currently encrypted to a single key that only I hold, which is incompatible with automatic release. Part of this work is a one-off re-encryption of the historical archive. The release job should be able to decrypt only the submission due for release, not the whole archive; its credentials must not enter a public workflow. At least two maintainers should be able to recover or rotate the release keys. The exact key scheme is an implementation decision subject to a security review.

On web search and training-data contamination: several people have proposed standardized blocklists or verified clean-run protocols. I don't think we can referee that from here; we can't observe anyone's harness. Instead we collect the structured self-report above and display it, so consumers of the leaderboard can filter by claimed methodology. If a lab wants to demonstrate a clean run, the methodology fields give them a place to say so.

Release also permits downstream reuse in Mathlib, LeanPool, and TauCeti. This plan does not assign that downstream work.

5. Copycat detection (deferred)

We've had submissions that were substantially copies of already-public solutions, and I've handled them by hand. An automated rejection scheme (normalized compression distance against all prior submissions, calibrated on the corpus) was drafted for this plan and cut after review feedback: short proofs legitimately converge on near-identical text, a determined cheater can rewrite around any similarity measure, and the manual workload so far doesn't justify the machinery.

What remains instead: the publication policy makes copying harder to begin with (submissions are private, releases are delayed), and the leaderboard's emphasis on unique solves means a copied solution earns nothing distinctive. Egregious cases keep being handled by hand: an accepted copy receives an append-only retraction event and stops counting in standings; the base result is not deleted. Building on public prior work (reusing lemmas, following a published proof strategy) was never in question; it's what released solutions are for.

If wholesale copying becomes a practical problem again, any automation needs a fresh maintainer decision; it is not part of this overhaul.

6. Official-kernel and nanoda validation

New and historical submissions use the ordinary Lean build/elaboration path and nanoda. Historical replay restores the exact original benchmark, toolchain, comparator, lean4export, and nanoda pins and records terminal acceptance, checker rejection, orchestration failure, timeout, resource-limit, or unavailable outcomes.

Checker identity and revision remain versioned extension points so a later project can replay old submissions with another checker without migrating the archive again. Experimental checkers, checker promotion, corpus qualification, and persistent kernel harnesses are outside this overhaul.

7. The replay queue and solution statistics

One bounded replay path serves both terminal validation and the comparison data below.

Mechanics. The queue contains versioned tasks keyed by accepted submission and measurement configuration. Queue events are files in the state repo, and a GitHub Actions cron processes them. Retries have the same task ID and cannot create a second result. For each submission, the harness:

1. checks out the trusted generated workspace at benchmark_commit;
2. overlays only the accepted Submission.lean and Submission/ snapshot from the audit archive;
3. restores the original pinned toolchain and dependencies;
4. builds and checks through the same sandboxed path used for intake, with no credentials and no network available to submitter code;
5. runs the pinned official-kernel and nanoda checks; and
6. records terminal verdict, build/check cost, and size statistics.

The archive is not treated as a trusted Lake workspace. Historical toolchains, source dependencies, and required binary artifacts must be retained or mirrored; otherwise a replay is marked unavailable rather than silently moved to newer pins.

Public statistics. For every solution, the leaderboard will show:

• Checker replay instructions: instruction count of a designated reference checker replaying the export. Retired instructions are less noisy than wall-clock time on shared runners, but are not machine-independent.
• Build cost: instructions and wall-clock for building the submission workspace, i.e. elaboration cost.
• Size: lines of code and file count across Submission.lean and Submission/.

Every measurement records the toolchain, exporter and checker revisions, runner architecture, measurement command, cache state, and attempt number. Reference measurements use a pinned runner class; if its performance counters are unavailable, instruction counts are omitted rather than estimated. A new reference-checker or runner revision creates a new measurement series and does not overwrite the old one.

Each workspace replays under its original toolchain. Measurements are most comparable within one measurement series and toolchain era, and only approximately comparable across toolchain bumps. The toolchain is displayed as a field, but comparison tables remain flat unless the corpus replay shows a material toolchain effect. Problems with submissions spanning toolchains give an empirical estimate of that effect. Old submissions may require toolchain-specific lean4export builds.

The queue supports a new versioned measurement series when a retained component is re-pinned. Historical measurements remain available, while the current view uses the latest completed configuration.

Some very early submissions may predate the audit archive; we replay what we can and mark the rest.

8. The leaderboard

The frontend needs both new features and a sturdier architecture. The current site generates pages from Lean macros, and has twice hit recursion limits as the catalog grew (patched both times by Vasily, thank you).

Architecture. Keep Verso for the site shell, navigation, and prose pages, so we stay consistent with lean-lang.org. Move the data-heavy surfaces (problem tables, solution lists, comparison views) to client-side rendering from JSON. site-data/ already exists as the derived-data layer; it becomes the interface. Its schema is versioned and split into a small index plus per-group and per-problem files, so the browser need not load the full corpus. The client-side tables support sorting and filtering.

Features:

• Tabs are groups. Top-level navigation is the three groups (formalization evaluation, software verification, open problems). The two evaluation tabs state their submission policy. The open-problems tab has an intentional empty state and says that its content and submission policy have not yet been adopted.
• A scope selector within each tab, defaulting to the flagship set. On the formalization evaluation tab: v1 | draft | archive, defaulting to v1. Named sets and current-status views may overlap. Standings and problem tables apply to the selected scope. When v2 exists it becomes the default and v1 remains available. A selector with a single option is not rendered.
• Tag chips and filters. Problem rows show their tag chips; a tag filter narrows the tab's problem list and recomputes the standings table for the filtered subset client-side. The filter persists in the URL, so "just the Annals problems" is a shareable link, and the tab already supplies the context, so a filtered view doesn't restate the group. Internally the frontend treats a tab as a pinned filter, letting tab and tag views share rendering code; the data model keeps group as its own required field.
• Unique-solve emphasis. Model standings are computed per (group, selected scope). The default leaderboard lists models ordered by number of unique solves (problems where that canonical credit identity is the only one with an accepted, unretracted solve), with a toggle to switch the ordering to total solves. Component models of an ensemble do not separately receive the solve. Each model's card shows unique, first, and total solve counts (a first solve is the earliest accepted solve of a problem, by acceptance-event order), leading with whichever the current sort uses. There is no combined cross-group leaderboard: the group scopes and policies are distinct, so their standings are not comparable. The front page shows headline numbers per tab instead.
• Recent solutions feed: a chronological page of new solves (problem, model, submitter, date, first-solve flag), from the materialized result and amendment view. It is global across groups, with group badges and a filter. It also has an RSS feed.
• Per-problem comparison pages: all solutions to a problem side by side with model, metadata, statistics from the replay harness, and links to released solutions. These pages support fixed-problem comparisons of models and harnesses.
• Metadata display with provenance: declared-at-submission vs backfilled, self-reported throughout, publication choice visible.
• Stable URLs: existing problem URLs (/eval/problems/<id>) keep working. A problem's page is permanent and status-agnostic: it shows the problem's group, current status, status history, and all solutions, so archived and resolved problems keep first-class pages. Meaningful statement revisions and retractions are visible on the same page.

9. Software verification

A new problem group, alongside formalization evaluation. It launches with every problem in draft status: no frozen set, problems added and revised freely. Standings shown but explicitly provisional; the group can freeze its own first set later, on its own schedule.

In scope, in rough order of arrival:

1. Theory-of-programs theorems: deep results about formal systems, in standard comparator shape. Two seed problems are drafted, posted as gists for comment: strong normalization and consistency for a calculus of constructions with a universe hierarchy, and quantifier elimination and a decision procedure for real closed fields.
2. Verified software artifacts: correctness theorems about executable programs (compilers, data structures, protocols), still comparator-checkable.
3. Verified calculations are deferred. Performance-ranked execution needs a later trusted-runner specification and infrastructure; neither is part of this overhaul.

10. The open-problems group

The third group is open problems: a provider-neutral catalog distinct from the evaluation groups. Its tab may launch empty, with a clear intentional empty state. Adding content later is an ordinary LeanEval-owned catalog decision.

This overhaul does not include an importer, external synchronization, provider-owned content lane, disproof semantics, or dependency on another project. Any future policy for submissions or resolved problems requires a separate maintainer decision.

Staging and migration

The current migration sequence is maintained only in docs/overhaul-execution-runbook.md. Production intake, replay, publication, and public lifecycle APIs remain approval-gated. Server intake launches alongside issue intake; issue intake is retired only after the four-week overlap, two-week notice, stability, adoption, and final historical-cutoff gates pass.

Immutable base Results remain in lean-eval-submissions; the lifecycle-aware site combines them with append-only State. Historical replay uses exact official-kernel and nanoda pins and may proceed in parallel with the overlap.

Workstreams

The active workstreams are:

1. Official-kernel and nanoda replay: archive restore, exact-pin builds, terminal outcomes, statistics, and bounded queue mechanics.
2. Submission lifecycle: server intake, append-only State, owner and maintainer routes, one-way release scheduling, pause, and rollback.
3. Archive and release: per-submission envelopes, separated wrap/unwrap authority, deterministic reconstruction, and automatic publication.
4. Lifecycle-aware leaderboard: group tabs, stable problem pages and statements, standings, metadata, statistics, and released solutions.
5. Historical completion: final cutoff, public/private/unavailable classification, private-envelope migration, and replay.
6. Remaining product work: neutral open-problems empty state and the two reviewed software-verification drafts.
7. Human-owned work: credential ceremonies and final statement, citation, background, and hint review.

Questions outside those lanes require a new maintainer scope decision; they are not latent work for this overhaul.