From 3779ddc71a1c10f0dca8df602ff43e17ae6e890e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 19 Aug 2026 08:07:38 +0000 Subject: [PATCH 1/5] doc: replace PLAN.md with the LeanEval overhaul plan Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ --- PLAN.md | 812 ++++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 793 insertions(+), 19 deletions(-) diff --git a/PLAN.md b/PLAN.md index 52a391354..857ee7fd9 100644 --- a/PLAN.md +++ b/PLAN.md @@ -1,25 +1,799 @@ -# PLAN +# LeanEval overhaul plan -This file tracks problem-set work that should be designed carefully -rather than improvised. +Status: **request for comment**. Written 2026-08-19. -The submission pipeline now lives in -[`leanprover/lean-eval-submissions`](https://github.com/leanprover/lean-eval-submissions); -roadmap items for it belong there. External version pins are done and -their bump procedure is documented in [`SECURITY.md`](SECURITY.md) §5. +This document plans a coordinated overhaul across the LeanEval repositories: -## Problem curation +- [leanprover/lean-eval](https://github.com/leanprover/lean-eval), the problem set, + generator, and comparator integration; +- [leanprover/lean-eval-submissions](https://github.com/leanprover/lean-eval-submissions), + the submission pipeline and results store; +- [leanprover/lean-eval-leaderboard](https://github.com/leanprover/lean-eval-leaderboard), + the public site at ; +- [leanprover/lean-eval-audit](https://github.com/leanprover/lean-eval-audit) (private), + the encrypted archive of every evaluated submission. -The repo currently ships ~33 workspaces across number theory, combinatorics, -topology, complex analysis, group theory, convex geometry, linear algebra, -algebraic geometry, differential geometry, and a couple of starter / hole -examples. +It also proposes two new repositories (a submission state repo and an extracted +generator), and one new service (a submission server). -Open work: +This document requests comments and volunteers. The +[Workstreams](#workstreams) section lists separable pieces of work. Nothing is +assigned yet. -- audit topic coverage and difficulty distribution (we are already past the - original 15–25 problem target, so the question is which problems are - carrying their weight) -- decide whether any problems are too easy or saturated by current frontier - models and should be retired or replaced -- continue adding problems where we identify gaps +Relevant discussion: +[#Model comparisons for Lean > LeanEval](https://leanprover.zulipchat.com/#narrow/channel/583341-Model-comparisons-for-Lean/topic/LeanEval), +[#Formal conjectures > Quality of life improvements](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Quality.20of.20life.20improvements), +and [lean-eval#533 formal-conjectures integration](https://github.com/leanprover/lean-eval/issues/533). + +## 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](https://github.com/leanprover/lean-eval/pull/532). +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. +- Several recently discovered kernel soundness bugs require accepted results + to be corroborated by more than one checker. +- 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). +- The Formal Conjectures project wants to integrate, and is offering real labor + to do it. + +## 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. **Reject copycat submissions** that are substantially identical to prior + solutions, including still-embargoed ones. +5. Validate submissions against **additional independent kernels** from the + [Lean Kernel Arena](https://arena.lean-lang.org), and promote checkers that + meet the required-validation criteria. +6. Build a **replay queue** that backfills soundness verdicts, re-checking + every historical accepted submission under the expanded kernel set as it + grows, and computes public per-solution statistics (instruction counts, + build cost, size) for all accepted submissions, past and future. +7. Rebuild the **leaderboard** with tabs, unique-solve emphasis, a recent + solutions feed, and per-problem comparison pages. +8. Open a **software verification** problem group, initially all-draft. +9. Add an **open conjectures** group, with content and ownership from the + Formal Conjectures project, and a single shared generator across the + projects. +10. Keep submission intake live throughout, then replace the old leaderboard + rather than maintaining long-term compatibility with it. + +Each goal gets a section below. The +[Staging and migration](#staging-and-migration) section explains ordering and +dependencies. + +## 1. Problem groups and lifecycle + +Four properties classify every problem: group, current status, frozen-set +membership, and visibility. + +**Group** is the subject-matter dimension, and there are three: formalization +evaluation (the current benchmark), software verification, and open +conjectures. Groups differ in audience and submission policy (embargoed release +for the first two, public submissions for open conjectures), and each gets its +own leaderboard tab. + +**Current status** is orthogonal to group. A problem is **draft**, **active**, +or **archived**. For open conjectures, an archived problem that was proved or +disproved is displayed as **resolved**; retracted or misformalised statements +remain distinguishable from genuine resolutions. + +- 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 conjectures will likely take sets directly from FC releases (FC100 Open +Set 1, and so on). 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 resolved conjecture therefore remains in every frozen set to which it +belongs, and its solves remain in those standings. Resolution changes its +current status, not its set membership. + +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. + +The leaderboard's site-data schema records group, current status, status +history, visibility, 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 + +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.** An LLM-assisted audit of the full catalog produces a candidate +cut list, which I'll review and decide on. The principles: + +- If many people have already solved a problem, we cut it from 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 is a cut (or a fix-then-keep). + +**What happens to cut problems.** They stay in the repository and keep +accepting submissions, but they move to 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](https://github.com/leanprover/lean-eval/pull/501) and + [lean-eval#502](https://github.com/leanprover/lean-eval/pull/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, including upstream fixes to Formal Conjectures +problems. 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; +- 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.) Open + conjecture submissions instead must be public from the start; see the open + conjectures section. +- **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 may opt out** at submission time or any time before release. + Opt-outs are recorded and displayed on the leaderboard entry ("solution + withheld"). The default is release; opting out is visible. +- **Existing submissions are grandfathered.** Their declared tiers stand. The + backfill mechanism includes an invitation to opt in to 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. +The append-only event order resolves an opt-out racing with release: an opt-out +recorded before the release transition prevents publication. 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](https://github.com/vasnesterov/LeanPool), and TauCeti. This plan does +not assign that downstream work. + +## 5. Copycat rejection + +We've already had submissions that were substantially copies of +already-public solutions. Under the new policy most solutions eventually +become public, and unique solves carry more leaderboard weight, so the +incentive to copy grows. + +**Measure.** Normalized compression distance (NCD) with zstd. The comparison +payload consists only of `Submission.lean` and files under `Submission/`, in a +canonical path order with explicit file separators. A lightweight lexer removes +comments and normalizes whitespace before compression. Identifier changes are +left to the compression metric rather than treated as exact renames. +For compressed size `C`, let +`Cpair(x,y) = min(C(x ++ sep ++ y), C(y ++ sep ++ x))`; the score is +`(Cpair(x,y) - min(C(x), C(y))) / max(C(x), C(y))`. The exact normalization, +separator, zstd version and settings, minimum-size rule, and threshold are +pinned and published. + +**Scope.** A new submission for problem P is compared against every previously +accepted submission for the same statement revision, public or private. The +acceptance-event order is authoritative when submissions overlap. Matches +against the same submitter's prior work are not treated as copying, although +the ordinary deduplication rules still prevent them from minting duplicate +solves. Model corrections use amendments rather than resubmission. When the +matched submission is public we name it in the rejection; when it is private, +the rejection says only that the submission is substantially identical to a +prior one. + +Comparison against private submissions necessarily reveals that a similar +prior submission exists. The response exposes no score, matched fragments, or +identity. We accept this limited leakage in order to enforce the same rule +before and after release. + +**Calibration before enforcement.** Since I can decrypt the audit archive, the +first step is an all-pairs similarity backtest over the full corpus: see where +known copies land versus legitimate independent solves, and pick thresholds +from data. We'll only flag submissions that are both large (small proofs +legitimately converge on near-identical text) and very similar. + +**Consequence.** A threshold match is rejected, automatically. There is no +dispute mechanism. Historical matches found during calibration are reported +to me. An egregious accepted copy receives an append-only retraction event +and stops counting in standings; the base result is not deleted. + +This targets egregious wholesale copying only. Building on public prior work +(reusing lemmas, following a published proof strategy) is not what this +catches, and is not banned; it's what released solutions are for. + +## 6. Independent kernel validation + +After the recent soundness discoveries, this is a priority: as well as the +standard kernel and nanoda, test submissions against a selection of the +experimental kernels at the +[Lean Kernel Arena](https://arena.lean-lang.org), collecting both acceptance +and performance data. A checker is eligible for **required validation** when it +has no incorrect arena verdicts, supports every construct used by the current +corpus, agrees with the adjudicated corpus verdicts, and runs in reasonable +time. Timeouts and explicitly unsupported tests are recorded separately from +incorrect acceptance or rejection. + +**Where the arena stands** (snapshot 2026-08-18, 19 checkers, 193 tests): + +- Only `official-nightly` is clean on every test. The stable official kernel + fails three soundness tests (fixed in nightly); this is exactly why we want + checker diversity. +- `lean4lean` has no soundness failures (its one failure is a performance + test) and runs the full Mathlib export in about 1.6x the official-nightly + wall time. It's the leading promotion candidate today. +- The fast Rust checkers (`sokonanoda`, `zignodamus`, `mathgraph`, `nanoclo`, + 10x to 40x faster than official on the Mathlib export) each fail exactly one + soundness test (`extra-rec`). Each is one fix away from candidacy, and we + should tell their authors so. +- `nanoda`, which we already require, has zero incorrect results but declines + nine tests. Note also that the arena pins a different nanoda fork and + revision than we do; the pins should be reconciled. + +**Plan.** + +- **Close known holes first.** Before the broader replay, check each known + stable-kernel failure against the current official-plus-nanoda required + checks. If a + known exploit passes both, update the required pin or temporarily reject the + affected construct before accepting more submissions. +- **Backtest immediately.** I'll decrypt the audit archive; the replay queue + (next section) exports each historical submission once and fans the export + out to candidate checkers. This yields acceptance and performance data over + the whole corpus right away, and doubles as the historical re-validation + under patched kernels that several people have asked for. +- **Shadow mode for new submissions.** Candidate checkers run on every new + submission after acceptance, recording verdicts without affecting them. Any + disagreement between checkers on a real submission triggers a soundness + investigation. A rejection may indicate either a bad submission or an + incomplete checker; raw agreement with comparator is not the criterion. +- **Adjudication.** Each disagreement gets a recorded resolution with checker, + exporter, and toolchain revisions. A historical result found invalid receives + a retraction event, stops counting in standings, and remains visible with the + reason. A corrected submission may be evaluated as a new result. +- **Promotion.** A checker becomes required when it satisfies the eligibility + conditions above and runs within budget (roughly: up to 3x the official + kernel is acceptable). +- **Required-checker failures.** Every required checker must accept a new + submission. A rejection, decline, crash, or timeout blocks automatic + acceptance and opens an incident. A checker that no longer supports the + allowed submission language is demoted until fixed rather than silently + narrowing the benchmark. +- **Pinning.** We build candidate checkers from source at pinned revisions + under the SECURITY.md regime and run them sandboxed, the same discipline as + the existing tools. We use the arena's published results to select + candidates, but we don't trust its binaries or its unsandboxed runs for our + validation path. + +**Export-format caveat.** The lean4export NDJSON format is +[still in flux](https://github.com/leanprover/lean4export/issues/3), and every +checker was written against some version of it. The plan pins an exporter and +checker revision matrix, not just checker revisions. A format mismatch is +reported separately from a checker verdict. + +All candidate checkers currently share lean4export, so checker diversity does +not cover bugs in the exporter or comparator's Challenge/Solution comparison. +That common dependency remains in the trust base and is versioned in every +verdict. An independent export path would reduce this residual risk, but is not +a prerequisite for the first checker promotions. + +## 7. The replay queue and solution statistics + +One harness serves both the kernel work above 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 exports through the same sandboxed path used for intake, with no + credentials and no network available to submitter code; +5. fans the export out to each candidate checker, recording verdict, + wall-clock, and retired-instruction counts; +6. records build 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 isn't one-shot: when a new candidate checker joins or an existing one +is re-pinned, the corpus receives new tasks for that checker configuration. +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 conjectures), each + stating its submission policy on the tab. +- **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: for example, a resolved + conjecture remains in its FC100 set and also appears under `resolved`. + 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. +- **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 both + numbers, leading with whichever the current sort uses. There is no combined + cross-group leaderboard: the groups have different submission policies, 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, opt-out status visible. +- **Stable URLs**: existing problem URLs (`/eval/problems/`) 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](https://gist.github.com/kim-em/ede78934812e777e75836f6c5509f769), + and + [quantifier elimination and a decision procedure for real closed + fields](https://gist.github.com/kim-em/5c2b7d45dbcc13970b13e49bf2251165). +2. **Verified software artifacts**: correctness theorems about executable + programs (compilers, data structures, protocols), still + comparator-checkable. +3. **Verified calculations**: performance-ranked verified implementations + ("fastest verified X"). This needs + execution and timing infrastructure that comparator doesn't have, so it's + in scope but phased last; the draft group permits prototyping before a + frozen set is defined. Before accepting these submissions we need a separate + specification of trusted inputs, sandboxing, runner hardware, repetitions, + resource limits, and anti-specialization rules. + +## 10. The open conjectures group + +The third group is **open conjectures**: statements with no known proof. The +tab is not branded around any one source, but the content is expected to come +overwhelmingly from the +[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) +project, which has offered to integrate its problem sets, starting with the +frozen FC100 open list (one hundred open conjectures). The FC contributors +are interested in owning this part of lean-eval. I propose giving them merge +rights for problem PRs in the group. Coordination: +[lean-eval#533](https://github.com/leanprover/lean-eval/issues/533) and +[formal-conjectures#4930](https://github.com/google-deepmind/formal-conjectures/issues/4930). + +**Submission policy.** Open conjectures differ from problems with known +informal solutions: + +- **Public submissions required from the start.** A claimed solution to an + open conjecture must be inspectable, especially because misformalisation is + a risk. No embargo, no opt-out; the submission URL and exact commit must be + public. We still archive the accepted snapshot, so later repository changes + cannot change the evaluated source. +- **Only open conjectures go in this group.** FC's research-solved statements + (formalized theorems without a recorded formal proof) don't get their own + policy or tab; the only role for them here is as a future source of + candidate problems for the benchmark's draft group. +- **Resolution.** A conjecture becomes resolved when it is proved or disproved. + It leaves the current open-problem view but remains in every frozen set to + which it belongs, and its solves remain in those standings. Retraction as + misformalised is recorded separately from resolution. Resolved conjectures + may continue to accept independent submissions. +- **Disproofs allowed.** A proof of the negation is as + valuable as a proof. This needs the comparator disproof support in + [Auguste's branch](https://github.com/augustepoiroux/comparator/tree/upstream/disproofs) + to be upstreamed; there are known universe-level subtleties (Eric Wieser has + thought about these). The FC integration motivates this comparator + workstream. + +**One generator.** The projects use one workspace generator. The generator +core currently inside `EvalTools` +(the part that turns a marked-up Lean module plus a manifest into a Challenge / +Solution / Submission workspace, with all the import- and scope-fidelity work +from [lean-eval#531](https://github.com/leanprover/lean-eval/pull/531)) gets +extracted into its own repository (working name: +`leanprover/lean-eval-generator`), consumed as a pinned dependency by lean-eval +and by the FC importer. The FC importer does not fork the generation logic. + +**Hosting: vendored, FC-owned importer.** FC problems are vendored into +lean-eval like every other problem. LeanEval remains the trusted statement +repository and supplies the pin regime and CI. The FC side owns an importer +(evolving their existing +[formal-conjectures#4951](https://github.com/google-deepmind/formal-conjectures/pull/4951) +adapter) that maps FC declarations and metadata to LeanEval modules and +manifests, and emits PRs to lean-eval that our CI validates like any other +problem PR. Each manifest records the FC source commit and declaration ID. When +FC fixes a misformalisation upstream, the importer regenerates and PRs the +corrected revision. The statement-revision policy above determines the +treatment of existing solves. + +**Technical extensions needed**, in dependency order: + +1. generator extraction (above); +2. definition holes / `answer(sorry)`: already supported; +3. disproof support: comparator upstreaming, then generator and manifest + support for "prove or disprove" problems; +4. multi-file Challenge support (imports between trusted files), which the + generator partially has via `ChallengeDeps` and comparator constrains; + scope this with the FC folks against the actual FC100 statements rather + than in the abstract. + +Several FC contributors have said they have time for this now, with more +available around the September workshop. + +## Staging and migration + +Submission intake remains live throughout. The old leaderboard may temporarily +omit or misclassify new statuses, amendments, and groups during the short +migration; it will be taken offline after the new site replaces it. We do not +maintain a compatibility layer for it. + +Two interfaces support the migration: + +- Immutable base results remain in lean-eval-submissions. The new site-data + build combines them with the append-only state events; the old site may + continue to read only the base results until replacement. +- New validators start in shadow. The replay queue, extra checkers, and copycat + detector run on accepted submissions before any of them affects a verdict. + +**Phase 0, immediately (independent of everything else):** + +- Create the state repo and event/materialization skeleton. Stand up the replay + harness; decrypt and replay the audit archive. +- Kernel backtesting and copycat calibration use the replay output. +- Output: corpus-wide soundness report, candidate-checker evidence, + similarity thresholds, and the first statistics dataset. + +**Phase 1, before the switchover (problem-set side):** + +- v1 audit, cut decisions, freeze declared in the repo, with current statuses + and v1 membership established alongside it. +- Software verification seed problems merge (draft status needs no freeze). +- Generator extraction can start any time; it must land before FC import PRs. + +**Phase 2, the submission server:** + +- Build the Worker and operator CLI against the state repo; new intake goes live + alongside issue intake, both writing the base-results store. +- The publication policy takes effect for submissions through the server (the + server is what collects the acknowledgements and runs the release + countdown). Backfill, rename, and repair open here too. +- Copycat rejection turns on as an intake check once calibrated. (If + calibration finishes early, it can run as a check in the existing issue + pipeline first.) +- After a four-week deprecation window, issue intake closes. + +**Phase 3, the leaderboard:** + +- Build the new site (tabs, client-side tables, unique solves, recent feed, + comparison pages) against the extended site-data schema, deployed to a + preview URL while the current site keeps its daily deploys. +- Deploy once the new site renders the full materialized view correctly. Keep + the previous deployment available for rollback during the switchover. Old + problem URLs keep working on the new site; other old-site compatibility is + not a goal. + +**Phase 4, open conjectures:** + +- Policy and importer design settle in the coordination issues; the first + FC100 import appears as the open-conjectures tab. +- Disproof support follows comparator upstreaming and need not block the + first import (open conjectures can launch proof-only and gain disproofs). + +**Checker promotion** is not a phase; it happens whenever the evidence from +Phase 0 justifies it, independent of everything else. + +These phases are a dependency order, not a calendar, and much of the work can +run concurrently. The target leaderboard migration window is about one week; +the issue-intake deprecation may continue after the site replacement. +Submission intake stays open, and the new site replaces the old one after +full-store validation. + +## Workstreams + +Separable pieces, in no particular order. None of these are assigned. Volunteer +on +[lean-eval#533](https://github.com/leanprover/lean-eval/issues/533) for FC +work or on the Zulip threads above for everything else. + +The default, for anything nobody claims: I'll point Sol at the bulk of this +list. The exceptions are 9 and 10, which belong with the Formal Conjectures +and comparator contributors respectively, and 13, which is human-written by +design. Human hands also stay on the key ceremony in 6 and on final review of +trusted problem statements in 11. + +1. **Replay harness**: audit-archive restore, original-pin builds, export, + checker fan-out, statistics capture, queue mechanics. +2. **Kernel backtesting**: run candidates over the corpus, chase + disagreements, reconcile our nanoda pin with the arena's, report + `extra-rec` status to the fast-checker authors, assemble promotion cases. +3. **Copycat calibration**: all-pairs NCD over the corpus, threshold + selection, the intake check. +4. **v1 audit**: LLM-assisted catalog review producing the candidate cut list + with evidence (solve counts, known leaks, misformalisation risk). +5. **Problem metadata**: group, status, visibility, statement revisions, + frozen-set membership and history, validation, and migration of the current + catalog. +6. **Submission server**: Worker, state repo and materializer, operator CLI, + OAuth and agent paths, GitHub App snapshots, amendment/repair records, + release countdown, archive publication, and the audit-archive key changes + that automatic release requires. +7. **Leaderboard v2**: extended site-data schema, canonical model identities, + client-side tables, tabs, unique-solve standings, recent feed, comparison + pages. +8. **Generator extraction**: factor the generator core out of `EvalTools` + into its own repo, consumed by lean-eval and the FC importer. +9. **FC importer**: FC-side, evolving + [formal-conjectures#4951](https://github.com/google-deepmind/formal-conjectures/pull/4951) + to emit lean-eval problem PRs through the shared generator. +10. **Comparator disproof support**: upstream + [Auguste's branch](https://github.com/augustepoiroux/comparator/tree/upstream/disproofs), + resolve the universe questions, then generator/manifest support. +11. **Software verification problems**: author and review problems for the + draft group; design the verified-calculations execution infrastructure. +12. **Policy text**: the submitter-facing versions of the publication policy, + license acknowledgement, copycat policy, and metadata forms. +13. **Flavour text review**: uniform informal statements and + citations/literature background across the catalog, plus hints where + authors have them (human-written only). + +## Open questions + +Feedback is particularly welcome on: + +1. Is two months the right embargo length? +2. Which comparison statistics matter to you beyond instruction counts, build + cost, and size? +3. Is there appetite among the fast-checker authors to fix `extra-rec` and + join the required-validation set? From 8c7360335adbc60a942c8a2bad8498c499022c7a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 19 Aug 2026 08:07:49 +0000 Subject: [PATCH 2/5] doc: link the request-for-comment PR from the status line Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ --- PLAN.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/PLAN.md b/PLAN.md index 857ee7fd9..628f37c0a 100644 --- a/PLAN.md +++ b/PLAN.md @@ -1,6 +1,8 @@ # LeanEval overhaul plan -Status: **request for comment**. Written 2026-08-19. +Status: **request for comment**, on +[lean-eval#536](https://github.com/leanprover/lean-eval/pull/536). +Written 2026-08-19. This document plans a coordinated overhaul across the LeanEval repositories: From 15ac43929e97008c31c3538aade0c23cd198196f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 19 Aug 2026 12:00:56 +0000 Subject: [PATCH 3/5] doc: add tags as an orthogonal, policy-free problem dimension Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ --- PLAN.md | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/PLAN.md b/PLAN.md index 628f37c0a..111734ad7 100644 --- a/PLAN.md +++ b/PLAN.md @@ -88,8 +88,8 @@ dependencies. ## 1. Problem groups and lifecycle -Four properties classify every problem: group, current status, frozen-set -membership, and visibility. +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 @@ -125,8 +125,18 @@ 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, and frozen-set memberships. Result records remain +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. @@ -548,6 +558,13 @@ The client-side tables support sorting and filtering. 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 @@ -765,8 +782,9 @@ trusted problem statements in 11. 4. **v1 audit**: LLM-assisted catalog review producing the candidate cut list with evidence (solve counts, known leaks, misformalisation risk). 5. **Problem metadata**: group, status, visibility, statement revisions, - frozen-set membership and history, validation, and migration of the current - catalog. + frozen-set membership and history, tags and the tag registry (including + auto-derived topic-area tags and the `annals` backfill), validation, and + migration of the current catalog. 6. **Submission server**: Worker, state repo and materializer, operator CLI, OAuth and agent paths, GitHub App snapshots, amendment/repair records, release countdown, archive publication, and the audit-archive key changes From bfa99e983df1abf80312c952fd99f920906ea3d9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Aug 2026 01:09:43 +0000 Subject: [PATCH 4/5] doc: apply review decisions from PR discussion Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ --- PLAN.md | 151 +++++++++++++++++++++++--------------------------------- 1 file changed, 62 insertions(+), 89 deletions(-) diff --git a/PLAN.md b/PLAN.md index 111734ad7..50e5f0d55 100644 --- a/PLAN.md +++ b/PLAN.md @@ -64,23 +64,21 @@ The system works, but it's showing strain: 3. Introduce a **publication policy** for the evaluation groups: submissions are private, and released automatically after two months unless the submitter opts out. -4. **Reject copycat submissions** that are substantially identical to prior - solutions, including still-embargoed ones. -5. Validate submissions against **additional independent kernels** from the +4. Validate submissions against **additional independent kernels** from the [Lean Kernel Arena](https://arena.lean-lang.org), and promote checkers that meet the required-validation criteria. -6. Build a **replay queue** that backfills soundness verdicts, re-checking +5. Build a **replay queue** that backfills soundness verdicts, re-checking every historical accepted submission under the expanded kernel set as it grows, and computes public per-solution statistics (instruction counts, build cost, size) for all accepted submissions, past and future. -7. Rebuild the **leaderboard** with tabs, unique-solve emphasis, a recent +6. Rebuild the **leaderboard** with tabs, unique-solve emphasis, a recent solutions feed, and per-problem comparison pages. -8. Open a **software verification** problem group, initially all-draft. -9. Add an **open conjectures** group, with content and ownership from the +7. Open a **software verification** problem group, initially all-draft. +8. Add an **open conjectures** group, with content and ownership from the Formal Conjectures project, and a single shared generator across the projects. -10. Keep submission intake live throughout, then replace the old leaderboard - rather than maintaining long-term compatibility with it. +9. Keep submission intake live throughout, then replace the old leaderboard + rather than maintaining long-term compatibility with it. Each goal gets a section below. The [Staging and migration](#staging-and-migration) section explains ordering and @@ -147,18 +145,21 @@ 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.** An LLM-assisted audit of the full catalog produces a candidate -cut list, which I'll review and decide on. The principles: +**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: -- If many people have already solved a problem, we cut it from v1. Saturated +- 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 is a cut (or a fix-then-keep). +- Known or suspected misformalisation risk excludes a problem until fixed. -**What happens to cut problems.** They stay in the repository and keep -accepting submissions, but they move to archive status and don't count toward -v1 standings. Existing solve records are never removed. +**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 @@ -352,53 +353,27 @@ Release also permits downstream reuse in Mathlib, [LeanPool](https://github.com/vasnesterov/LeanPool), and TauCeti. This plan does not assign that downstream work. -## 5. Copycat rejection - -We've already had submissions that were substantially copies of -already-public solutions. Under the new policy most solutions eventually -become public, and unique solves carry more leaderboard weight, so the -incentive to copy grows. - -**Measure.** Normalized compression distance (NCD) with zstd. The comparison -payload consists only of `Submission.lean` and files under `Submission/`, in a -canonical path order with explicit file separators. A lightweight lexer removes -comments and normalizes whitespace before compression. Identifier changes are -left to the compression metric rather than treated as exact renames. -For compressed size `C`, let -`Cpair(x,y) = min(C(x ++ sep ++ y), C(y ++ sep ++ x))`; the score is -`(Cpair(x,y) - min(C(x), C(y))) / max(C(x), C(y))`. The exact normalization, -separator, zstd version and settings, minimum-size rule, and threshold are -pinned and published. - -**Scope.** A new submission for problem P is compared against every previously -accepted submission for the same statement revision, public or private. The -acceptance-event order is authoritative when submissions overlap. Matches -against the same submitter's prior work are not treated as copying, although -the ordinary deduplication rules still prevent them from minting duplicate -solves. Model corrections use amendments rather than resubmission. When the -matched submission is public we name it in the rejection; when it is private, -the rejection says only that the submission is substantially identical to a -prior one. - -Comparison against private submissions necessarily reveals that a similar -prior submission exists. The response exposes no score, matched fragments, or -identity. We accept this limited leakage in order to enforce the same rule -before and after release. - -**Calibration before enforcement.** Since I can decrypt the audit archive, the -first step is an all-pairs similarity backtest over the full corpus: see where -known copies land versus legitimate independent solves, and pick thresholds -from data. We'll only flag submissions that are both large (small proofs -legitimately converge on near-identical text) and very similar. - -**Consequence.** A threshold match is rejected, automatically. There is no -dispute mechanism. Historical matches found during calibration are reported -to me. An egregious accepted copy receives an append-only retraction event -and stops counting in standings; the base result is not deleted. - -This targets egregious wholesale copying only. Building on public prior work -(reusing lemmas, following a published proof strategy) is not what this -catches, and is not banned; it's what released solutions are for. +## 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, the drafted scheme is +in this document's history and can be revived. ## 6. Independent kernel validation @@ -621,7 +596,10 @@ In scope, in rough order of arrival: ## 10. The open conjectures group -The third group is **open conjectures**: statements with no known proof. The +The third group is **open conjectures**: statements with no known proof. This +group is **not an evaluation set**, and the site displays and describes it +differently from the evaluation groups, keeping claims about model capability +and claims about progress on open problems clearly separate. The tab is not branded around any one source, but the content is expected to come overwhelmingly from the [Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) @@ -703,16 +681,16 @@ Two interfaces support the migration: - Immutable base results remain in lean-eval-submissions. The new site-data build combines them with the append-only state events; the old site may continue to read only the base results until replacement. -- New validators start in shadow. The replay queue, extra checkers, and copycat - detector run on accepted submissions before any of them affects a verdict. +- New validators start in shadow. The replay queue and extra checkers run on + accepted submissions before either affects a verdict. **Phase 0, immediately (independent of everything else):** - Create the state repo and event/materialization skeleton. Stand up the replay harness; decrypt and replay the audit archive. -- Kernel backtesting and copycat calibration use the replay output. -- Output: corpus-wide soundness report, candidate-checker evidence, - similarity thresholds, and the first statistics dataset. +- Kernel backtesting uses the replay output. +- Output: corpus-wide soundness report, candidate-checker evidence, and the + first statistics dataset. **Phase 1, before the switchover (problem-set side):** @@ -728,9 +706,6 @@ Two interfaces support the migration: - The publication policy takes effect for submissions through the server (the server is what collects the acknowledgements and runs the release countdown). Backfill, rename, and repair open here too. -- Copycat rejection turns on as an intake check once calibrated. (If - calibration finishes early, it can run as a check in the existing issue - pipeline first.) - After a four-week deprecation window, issue intake closes. **Phase 3, the leaderboard:** @@ -767,44 +742,42 @@ on work or on the Zulip threads above for everything else. The default, for anything nobody claims: I'll point Sol at the bulk of this -list. The exceptions are 9 and 10, which belong with the Formal Conjectures -and comparator contributors respectively, and 13, which is human-written by -design. Human hands also stay on the key ceremony in 6 and on final review of -trusted problem statements in 11. +list. The exceptions are 8 and 9, which belong with the Formal Conjectures +and comparator contributors respectively, and 12, which is human-written by +design. Human hands also stay on the key ceremony in 5 and on final review of +trusted problem statements in 10. 1. **Replay harness**: audit-archive restore, original-pin builds, export, checker fan-out, statistics capture, queue mechanics. 2. **Kernel backtesting**: run candidates over the corpus, chase disagreements, reconcile our nanoda pin with the arena's, report `extra-rec` status to the fast-checker authors, assemble promotion cases. -3. **Copycat calibration**: all-pairs NCD over the corpus, threshold - selection, the intake check. -4. **v1 audit**: LLM-assisted catalog review producing the candidate cut list +3. **v1 audit**: LLM-assisted catalog review producing the candidate list with evidence (solve counts, known leaks, misformalisation risk). -5. **Problem metadata**: group, status, visibility, statement revisions, +4. **Problem metadata**: group, status, visibility, statement revisions, frozen-set membership and history, tags and the tag registry (including auto-derived topic-area tags and the `annals` backfill), validation, and migration of the current catalog. -6. **Submission server**: Worker, state repo and materializer, operator CLI, +5. **Submission server**: Worker, state repo and materializer, operator CLI, OAuth and agent paths, GitHub App snapshots, amendment/repair records, release countdown, archive publication, and the audit-archive key changes that automatic release requires. -7. **Leaderboard v2**: extended site-data schema, canonical model identities, +6. **Leaderboard v2**: extended site-data schema, canonical model identities, client-side tables, tabs, unique-solve standings, recent feed, comparison pages. -8. **Generator extraction**: factor the generator core out of `EvalTools` +7. **Generator extraction**: factor the generator core out of `EvalTools` into its own repo, consumed by lean-eval and the FC importer. -9. **FC importer**: FC-side, evolving +8. **FC importer**: FC-side, evolving [formal-conjectures#4951](https://github.com/google-deepmind/formal-conjectures/pull/4951) to emit lean-eval problem PRs through the shared generator. -10. **Comparator disproof support**: upstream +9. **Comparator disproof support**: upstream [Auguste's branch](https://github.com/augustepoiroux/comparator/tree/upstream/disproofs), resolve the universe questions, then generator/manifest support. -11. **Software verification problems**: author and review problems for the +10. **Software verification problems**: author and review problems for the draft group; design the verified-calculations execution infrastructure. -12. **Policy text**: the submitter-facing versions of the publication policy, - license acknowledgement, copycat policy, and metadata forms. -13. **Flavour text review**: uniform informal statements and +11. **Policy text**: the submitter-facing versions of the publication policy, + license acknowledgement, and metadata forms. +12. **Flavour text review**: uniform informal statements and citations/literature background across the catalog, plus hints where authors have them (human-written only). From 499323425a4049732b92a768682927ddd63bb1b5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 20 Aug 2026 01:18:30 +0000 Subject: [PATCH 5/5] doc: collect prompts as metadata and show first-solve counts Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ --- PLAN.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/PLAN.md b/PLAN.md index 50e5f0d55..f1f1c0ade 100644 --- a/PLAN.md +++ b/PLAN.md @@ -267,6 +267,8 @@ produced" box: 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 @@ -545,8 +547,9 @@ The client-side tables support sorting and filtering. 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 both - numbers, leading with whichever the current sort uses. There is no combined + 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 groups have different submission policies, so their standings are not comparable. The front page shows headline numbers per tab instead.