From bdc21d5685b4f1d9b21531828d8f629330a2c815 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 25 Aug 2026 23:07:10 +0000 Subject: [PATCH] Align overhaul scope and catalog lifecycle --- PLAN.md | 433 ++++-------------- docs/catalog-metadata.md | 2 +- docs/overhaul-execution-runbook.md | 72 +-- .../problems/coc_strong_normalization.toml | 7 +- .../problems/rcf_quantifier_elimination.toml | 7 +- scripts/validate_catalog.py | 2 +- tests/python/test_validate_catalog.py | 15 + 7 files changed, 170 insertions(+), 368 deletions(-) diff --git a/PLAN.md b/PLAN.md index ef57f8473..a24b27343 100644 --- a/PLAN.md +++ b/PLAN.md @@ -1,8 +1,9 @@ # LeanEval overhaul plan -Status: **accepted for staged implementation**. The original RFC was reviewed -and merged in [lean-eval#536](https://github.com/leanprover/lean-eval/pull/536). -Written 2026-08-19; status updated 2026-08-20. +Status: **retained product-design reference; superseded for execution**. The +original RFC was reviewed and merged in +[lean-eval#536](https://github.com/leanprover/lean-eval/pull/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](docs/overhaul-completion-plan.md) and its @@ -20,12 +21,9 @@ 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 preserves the original design discussion. Resolved decisions and -implementation sequencing live in the -[public implementation program](https://gist.github.com/kim-em/cd6ac1c049f459ef9aa37d6cf551d9e4) -and the [implementation tracker](https://github.com/leanprover/lean-eval/issues/541); -where they differ from an unresolved proposal below, the recorded decision is -authoritative. +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: @@ -41,14 +39,11 @@ This document plans a coordinated overhaul across the LeanEval repositories: It also proposes two new repositories (a submission state repo and an extracted generator), and one new service (a submission server). -The [Workstreams](#workstreams) section records the original decomposition; -current ownership and completion state are maintained in the implementation -tracker. +The [Workstreams](#workstreams) section records the retained decomposition; +current completion state is maintained in the execution runbook. -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). +Relevant retained-product discussion: +[#Model comparisons for Lean > LeanEval](https://leanprover.zulipchat.com/#narrow/channel/583341-Model-comparisons-for-Lean/topic/LeanEval). ## Where things stand @@ -68,16 +63,13 @@ The system works, but it's showing strain: 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. +- 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). -- The Formal Conjectures project wants to integrate, and is offering real labor - to do it. ## Goals at a glance @@ -87,21 +79,18 @@ 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. 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. -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. +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 an **open conjectures** group, with content and ownership from the - Formal Conjectures project, and a single shared generator across the - projects. -9. Keep submission intake live throughout, then replace the old leaderboard - rather than maintaining long-term compatibility with it. +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](#staging-and-migration) section explains ordering and @@ -113,15 +102,14 @@ 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 -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. +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**. For open conjectures, an archived problem that was proved or -disproved is displayed as **resolved**; retracted or misformalised statements -remain distinguishable from genuine resolutions. +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. @@ -132,16 +120,12 @@ remain distinguishable from genuine resolutions. **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. +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 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. @@ -215,9 +199,8 @@ 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. +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 @@ -405,87 +388,26 @@ 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 - -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. +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 harness serves both the kernel work above and the comparison data below. +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 @@ -496,11 +418,10 @@ create a second result. For each submission, the harness: 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 +4. builds and checks 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. +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; @@ -532,10 +453,9 @@ 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. +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. @@ -557,13 +477,13 @@ 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. + (formalization evaluation, software verification, open problems), each + stating its submission policy on the tab. The open-problems tab has an + intentional empty state until LeanEval-owned content is added later. - **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 + 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 @@ -620,207 +540,52 @@ In scope, in rough order of arrival: 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. 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) -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: +3. **Verified calculations** are deferred. Performance-ranked execution needs + a later trusted-runner specification and infrastructure; neither is part of + this overhaul. -- 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 and extra checkers run on - accepted submissions before either affects a verdict. +## 10. The open-problems group -**Phase 0, immediately (independent of everything else):** +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. -- Create the state repo and event/materialization skeleton. Stand up the replay - harness; decrypt and replay the audit archive. -- Kernel backtesting uses the replay output. -- Output: corpus-wide soundness report, candidate-checker evidence, and the - first statistics dataset. +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. -**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. -- 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). +## Staging and migration -**Checker promotion** is not a phase; it happens whenever the evidence from -Phase 0 justifies it, independent of everything else. +The current migration sequence is maintained only in +[`docs/overhaul-execution-runbook.md`](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. -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. +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 -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 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. **v1 audit**: LLM-assisted catalog review producing the candidate list - with evidence (solve counts, known leaks, misformalisation risk). -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. -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. -6. **Lifecycle-aware leaderboard**: extended site-data schema, canonical model - identities, client-side tables, tabs, unique-solve standings, recent feed, - comparison pages. -7. **Generator extraction**: factor the generator core out of `EvalTools` - into its own repo, consumed by lean-eval and the FC importer. -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. -9. **Comparator disproof support**: upstream - [Auguste's branch](https://github.com/augustepoiroux/comparator/tree/upstream/disproofs), - resolve the universe questions, then generator/manifest support. -10. **Software verification problems**: author and review problems for the - draft group; design the verified-calculations execution infrastructure. -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). - -## 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? +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, release scheduling, opt-out, 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. diff --git a/docs/catalog-metadata.md b/docs/catalog-metadata.md index 3fdf22cf7..24d562e07 100644 --- a/docs/catalog-metadata.md +++ b/docs/catalog-metadata.md @@ -10,7 +10,7 @@ python scripts/validate_catalog.py ## Current fields - `group` is one of `formalization-evaluation`, `software-verification`, or - `open-conjectures`. + `open-problems`. - `status` is one of `draft`, `active`, or `archived`. - `visible` controls public catalog presentation independently of lifecycle. - `statement_revision` is a positive integer and never decreases. diff --git a/docs/overhaul-execution-runbook.md b/docs/overhaul-execution-runbook.md index 9cf759e68..f24245368 100644 --- a/docs/overhaul-execution-runbook.md +++ b/docs/overhaul-execution-runbook.md @@ -74,28 +74,28 @@ request. Goal: make the repositories describe only the approved remaining program. -- [ ] Inventory every open PR, active workflow, remote branch, and relevant +- [x] Inventory every open PR, active workflow, remote branch, and relevant local worktree in the allowlisted repositories. -- [ ] Confirm the already identified escaped external branches are absent and +- [x] Confirm the already identified escaped external branches are absent and the stale LeanEval PRs are closed. -- [ ] Review any uncommitted local cleanup attempt as an untrusted candidate +- [x] Review any uncommitted local cleanup attempt as an untrusted candidate diff. Keep useful pieces only after comparing them with current upstream. -- [ ] Delete the persistent model-identity qualification harness, private +- [x] Delete the persistent model-identity qualification harness, private qualification Workers, workflows, generated types, fixtures, tests, and rebuild/recovery instructions. -- [ ] Delete experimental-kernel shadow smoke, Arena/Mathgraph assets, +- [x] Delete experimental-kernel shadow smoke, Arena/Mathgraph assets, checker-series and corpus-promotion machinery, wire/attestation protocols, candidate adapters, and tests that exist only for them. -- [ ] Remove exact-byte solution-export capture hooks that existed only to feed +- [x] Remove exact-byte solution-export capture hooks that existed only to feed the removed experimental-kernel lane. -- [ ] Retain the existing official Lean build and nanoda replay path, its +- [x] Retain the existing official Lean build and nanoda replay path, its generic checker identity/revision fields, and its focused tests. -- [ ] Preserve source-bound agent sessions, authorization boundaries, +- [x] Preserve source-bound agent sessions, authorization boundaries, idempotency, CAS conflict handling, and other generally useful security hardening. - [ ] Remove superseded run narratives, diagnostic artifacts, and tests whose only purpose is preserving those narratives. -- [ ] Retain canonical replay inventories, final plans, exact toolchain/source +- [x] Retain canonical replay inventories, final plans, exact toolchain/source maps, unavailable-candidate data, current rollback contracts, and current infrastructure identifiers. - [ ] Retain an older canonical input set only while a live execution profile @@ -115,33 +115,46 @@ Goal: establish one exact safe baseline before launch work resumes. ### 5.1 Repositories and automation -- [ ] Record current protected `main` commits for every allowlisted repository. -- [ ] List open PRs and cross-referenced work; close or classify stale overhaul +- [x] Record current protected `main` commits for every allowlisted repository. +- [x] List open PRs and cross-referenced work; close or classify stale overhaul PRs. -- [ ] Confirm no unplanned workflow dispatch is queued or running. +- [x] Confirm no unplanned workflow dispatch is queued or running. - [ ] Confirm required checks, protected branches, and immutable dispatch-tag protections match current operating needs. +Current `main` baseline: + +| Repository | Commit | Protection state | +| --- | --- | --- | +| `lean-eval` | `de48559590eb8cff2125e8e933b3e13bb8a3ff98` | Required `verify` | +| `lean-eval-submissions` | `2bdeb2be1d1cd504a567dd01a3b040ae6e341827` | Required `verify` | +| `lean-eval-leaderboard` | `aef3269c7dd4a98781d7f2d9b23db3c196e14766` | Required `build` | +| `lean-eval-state` | `b0a30e3a64aa5c05660040405b32135dea4b7f1d` | Required `validate`; append-only | +| `lean-eval-state-staging` | `8d8ef8d1e30ac617d848c705907a941209aeb23c` | Required `validate`; append-only | +| `lean-eval-releases` | `90dadc872d624b8e6d171caf439313d185fc3e7f` | Required `validate` | +| `lean-eval-generator` | `77373a539b31f8f304c852f288d7d8469cceebff` | Required `check` | +| `lean-eval-audit` | `ad356e7bc5a2d650d9902ac3f6d352a0164360bc` | Protection approval required | + ### 5.2 Deployed services -- [ ] Read staging and production intake health. -- [ ] Read staging and production broker/replay health and current versions. -- [ ] Verify production intake is configured and effectively disabled. -- [ ] Verify general and production replay are disabled. -- [ ] Verify publication is disabled. -- [ ] Verify public lifecycle feature gates are disabled before their launch +- [x] Read staging and production intake health. +- [x] Read staging and production broker/replay health and current versions. +- [x] Verify production intake is configured and effectively disabled. +- [x] Verify general and production replay are disabled. +- [x] Verify publication is disabled. +- [x] Verify public lifecycle feature gates are disabled before their launch smoke and approval. -- [ ] Verify deployed commits, container image digests, and protected State pins +- [x] Verify deployed commits, container image digests, and protected State pins form one coherent current unit. ### 5.3 State, credentials, and presentation -- [ ] Verify protected State heads and validation status. +- [x] Verify protected State heads and validation status. - [ ] Inventory credential names, owners, scopes, expiry, rotation, and revocation without exposing values. -- [ ] Confirm production State contains no unexpected accepted server +- [x] Confirm production State contains no unexpected accepted server submission or due release work. -- [ ] Smoke the live leaderboard root, group tabs, stable problem URLs, +- [x] Smoke the live leaderboard root, group tabs, stable problem URLs, problem statements, and representative solution metadata. Exit condition: current documentation states one coherent disabled baseline. @@ -163,12 +176,12 @@ These lanes can proceed in parallel after Phase 1. ### 6.2 Release and archive repository preparation -- [ ] Reconfirm the exact staging release OIDC trust mismatch. -- [ ] Prepare the smallest reviewed infrastructure patch or operator command; +- [x] Reconfirm the exact staging release OIDC trust mismatch. +- [x] Prepare the smallest reviewed infrastructure patch or operator command; do not apply it yet. - [ ] Reconfirm the production archive Wrap-only role requirement and prove the desired policy excludes unwrap. -- [ ] Verify the release controller reconstructs deterministically with +- [x] Verify the release controller reconstructs deterministically with publication disabled using credential-free fixtures. - [ ] Verify submitter-facing license, release delay, and opt-out language. @@ -410,10 +423,10 @@ Update this table in place; do not append a history beneath it. | Phase | State | Current blocker | | --- | --- | --- | -| 0. Rebaseline cleanup | Not started | Review and merge scoped deletions | -| 1. Disabled baseline | Not started | Phase 0 | -| 2. Repository launch preparation | Not started | Phase 1 | -| Approval A. Staging credentials | Blocked on explicit approval | Exact mutation not yet presented | +| 0. Rebaseline cleanup | In progress | Stale-instruction cleanup PRs and final validation | +| 1. Disabled baseline | In progress | Audit-repository protection and credential inventory | +| 2. Repository launch preparation | In progress | Entry page, lifecycle gates, and bounded fixtures | +| Approval A. Staging credentials | Blocked on explicit approval | Exact staging trust mutation prepared but unapplied | | 3. Final staging acceptance | Not started | Approval A | | Approval B. Production launch | Blocked on explicit approval | Go/no-go packet incomplete | | 4. Launch | Not started | Approval B | @@ -421,4 +434,3 @@ Update this table in place; do not append a history beneath it. | 6. Historical completion | Not started | May begin after Phase 1; infrastructure steps approval-gated | | 7. Remaining product completion | Not started | Independent lanes; issue closure waits for overlap and final delta | | Final audit | Not started | All phases | - diff --git a/manifests/problems/coc_strong_normalization.toml b/manifests/problems/coc_strong_normalization.toml index 51d1f384d..0934cf3df 100644 --- a/manifests/problems/coc_strong_normalization.toml +++ b/manifests/problems/coc_strong_normalization.toml @@ -1,7 +1,7 @@ id = "coc_strong_normalization" title = "Strong normalization and consistency for the calculus of constructions with a universe hierarchy" group = "software-verification" -status = "active" +status = "draft" visible = true statement_revision = 1 tags = [] @@ -11,3 +11,8 @@ submitter = "Kim Morrison" source = "Coquand and Huet, 'The calculus of constructions' (1988); Zhaohui Luo, 'An Extended Calculus of Constructions' (1990); Bruno Barras, 'Sets in Coq, Coq in Sets' (2010)." notes = "Strong normalization requires Girard's reducibility candidates, and the impredicative `Prop` rule `(s, prop, prop)` is what makes a naive induction on types fail. The three anti-vacuity guards require a nonempty typing relation and exercise polymorphic typing, `Typing.app`, beta reduction, and substitution. Mathlib does not provide the requested Lean theorem; earlier Coq mechanizations and semantic models of CC and CCω are acknowledged in the module documentation." informal_solution = "Use reducibility candidates in the style of Girard, extended to dependent types and the predicative universe hierarchy. A smaller λC rehearsal replaces the hierarchy by `Prop` and a top sort `Type 0`; it is a different typing relation, not literally the restriction of this CCω syntax to two sorts." + +[[status_history]] +status = "draft" +effective_date = "2026-08-25" +reason = "correction" diff --git a/manifests/problems/rcf_quantifier_elimination.toml b/manifests/problems/rcf_quantifier_elimination.toml index 71772d841..16003474c 100644 --- a/manifests/problems/rcf_quantifier_elimination.toml +++ b/manifests/problems/rcf_quantifier_elimination.toml @@ -1,7 +1,7 @@ id = "rcf_quantifier_elimination" title = "Quantifier elimination for the theory of real closed fields" group = "software-verification" -status = "active" +status = "draft" visible = true statement_revision = 1 tags = [] @@ -11,3 +11,8 @@ submitter = "Kim Morrison" source = "Tarski, 'A Decision Method for Elementary Algebra and Geometry' (1951); Collins, 'Quantifier elimination for real closed fields by cylindrical algebraic decomposition' (1975); Mahboubi, 'Programming and certifying a CAD algorithm in the Coq system' (2006); Cohen and Mahboubi, 'Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination' (2012)." notes = "`isQF_qe` and `holds_qe` are jointly load-bearing; either alone admits a trivial implementation (`fun _ => .fals` and `id` respectively). Enumerating quantifier-free syntax is not a shortcut because recognizing an equivalent candidate already requires the substantive quantifier-elimination argument. The `holds_ex_sq` guard pins the intended de Bruijn and semantic interpretation. The pinned Mathlib dependency supplies real-closed-field algebra but not this `qe`; `Classical.choice` still requires first proving existence of a quantifier-free equivalent. A separate `valid?` hole was rejected as vulnerable to a one-line noncomputable implementation; see the module documentation." informal_solution = "The Cohen-Hormander route has a comparatively small formalization footprint; Cohen and Mahboubi's Coq development uses an algebraic pseudo-remainder route. Cylindrical algebraic decomposition is another practical route and has been formalized in Coq, including Mahboubi's work and the current MathComp CAD development." + +[[status_history]] +status = "draft" +effective_date = "2026-08-25" +reason = "correction" diff --git a/scripts/validate_catalog.py b/scripts/validate_catalog.py index 4204d233f..cbffa4041 100644 --- a/scripts/validate_catalog.py +++ b/scripts/validate_catalog.py @@ -15,7 +15,7 @@ PROBLEM_ID_RE = re.compile(r"^[A-Za-z0-9][A-Za-z0-9_-]*$") TAG_RE = re.compile(r"^[a-z0-9][a-z0-9-]*$") DIGEST_RE = re.compile(r"^sha256:[0-9a-f]{64}$") -GROUPS = {"formalization-evaluation", "software-verification", "open-conjectures"} +GROUPS = {"formalization-evaluation", "software-verification", "open-problems"} STATUSES = {"draft", "active", "archived"} REASONS = { "initial", diff --git a/tests/python/test_validate_catalog.py b/tests/python/test_validate_catalog.py index 59d0e20d1..8f47238ea 100644 --- a/tests/python/test_validate_catalog.py +++ b/tests/python/test_validate_catalog.py @@ -67,6 +67,21 @@ def test_valid_catalog(self): with temporary: self.assertEqual(VALIDATOR.validate(root), (1, 1, 0)) + def test_open_problems_is_the_neutral_catalog_group(self): + temporary, root = self.make_catalog( + PROBLEM.replace('group = "formalization-evaluation"', 'group = "open-problems"') + ) + with temporary: + self.assertEqual(VALIDATOR.validate(root), (1, 1, 0)) + + temporary, root = self.make_catalog( + PROBLEM.replace( + 'group = "formalization-evaluation"', 'group = "open-conjectures"' + ) + ) + with temporary, self.assertRaisesRegex(VALIDATOR.CatalogError, "unknown group"): + VALIDATOR.validate(root) + def test_unknown_tag_is_rejected(self): temporary, root = self.make_catalog(PROBLEM.replace('"annals"', '"unknown"')) with temporary, self.assertRaisesRegex(VALIDATOR.CatalogError, "unregistered tags"):