doc: replace PLAN.md with the LeanEval overhaul plan

[kim-em]

This PR replaces PLAN.md with the LeanEval overhaul planning document: the v1 problem set and problem lifecycle, a submission server with structured metadata and self-service amendments, a publication policy for the evaluation groups, copycat rejection, independent kernel validation via the Lean Kernel Arena, a replay queue with public per-solution statistics, the rebuilt leaderboard, the software verification and open conjectures groups, and staged migration.

It is a request for comment and for volunteers: please comment inline on anything you'd push back on, and claim workstreams you'd like to own.

🤖 Prepared with Claude Code

https://claude.ai/code/session_01H5aXYT6oHfUrx7EtBQuCBQ

[Vilin97]

@kim-em , thank you for the overhaul!

I will write down my (brief) feedback on https://github.com/kim-em/lean-eval/blob/8c7360335adbc60a942c8a2bad8498c499022c7a/PLAN.md.

I agree with goals 2, 3, 6, 7.
I disagree with 4.
I think we are missing another goal: adding harder and actually relevant problems. Right now a most of lean-eval is solvable with a single prompt (at least 180 problems but probably more). We need more problems, solving which requires developing a huge amount of theory that is completely missing from mathlib, on the order of at least 1M LOC or more.

More details below:

I do not see the need for incorporating formal conjectures, seeing that GDM's formal conjectures already exists. Unless the idea is to allow FC to use LeanEval's tooling such as the leaderboard and submission queue.

If many people have already solved a problem, we cut it from v1

I don't think we should modify a frozen set. If v1 came out to be too easy, we should make v2 harder.

I think the whole copycat reject scheme is the wrong way to go. It will have lots of false positives for short proofs. And if someone wants to cheat, it's trivial to just tell the models to alter the proof to circumvent the copycat filter. Instead we should have 2 mechanisms to deal with copycatting:

1. Make it easy to submit solutions privately and hard to leak them.
2. Celebrate first solves and unique solves in addition to total solves. The leaderboard should display how many first solves and how many unique solves a given submitter has, next to the total number of solves.

Which comparison statistics matter to you beyond instruction counts, build cost, and size?

The self-reported ones: token count, price, time-to-solve, prompt. There should be structured metadata collection for these fields. The prompt is important, because this is how we learn from each other what works and what doesn't.

[hanwenzhu]

My main concern with the current LeanEval is that it seems more like the scoreboard of a live competition rather than a fixed evaluation benchmark. It is hard to compare a certain score of model A from 2 months ago with a score of model B today, because problems are increasing, model A might publish solutions (especially with the new 2-month auto-release), model B may have spent more time on targeted searches of certain unsolved problems, etc. Score seems more like a function of interest instead of capability. If we emphasize unique or first solves more, this might worsen the issue.

I think copycat rejection is needed since solutions may eventually be public. I don't think there will be false positives if we tune correctly on the current solutions. Solutions can't possibly be enforced to always be private for the reasons: 1. LeanEval's problems intersect with TauCeti/Mathlib's roadmap (e.g. Hopf–Rinow) (and in this case it would even be better for the community if solutions were public under an OS license), and 2. if a company formalized a landmark result like FLT / unit distance conjecture / bounded prime gaps that is also on LeanEval, they would surely want to publish the formalization instead of keeping it private just to conform with LeanEval conventions. That is also why I think an internet blocklist would make sense; it makes the benchmark usable/comparable for quite a long time instead of 2 months.

[kim-em]

I do not see the need for incorporating formal conjectures, seeing that GDM's formal conjectures already exists. Unless the idea is to allow FC to use LeanEval's tooling such as the leaderboard and submission queue.

This is an explicit ask for the FC team. These problems will remain separate from the "leaderboard" group, and will be displayed / talked about differently to try to make clear they are not part of an evaluation set.

If many people have already solved a problem, we cut it from v1

I don't think we should modify a frozen set. If v1 came out to be too easy, we should make v2 harder.

I didn't intend it that way: I meant that if it has already been solved by many people (Aug 20!) it will never even enter "v1", which hasn't been determined yet. I'll make that clearer.

I think the whole copycat reject scheme is the wrong way to go.

Let me consult with others on this one. Note that we have already had problems with copy-pasted submissions, that I have been dealing with by hand. I would prefer to have some automation here. Note that the proposed plan calls for not applying this to short proofs. Nevertheless, mostly likely I will just cut this from the plan, deferring it until/unless the problem arises again in practice.

[kim-em]

because problems are increasing

This is the reason why we are going to declare an immutable "v1" problem set. This won't be a problem anymore.

[williamjblair]

Restructured formal-conjectures#4951 around the split in this plan.

• The FC side resolves the source declaration, dependencies, answer(sorry) slots, and provenance.
• The shared generator owns workspace generation; LeanEval owns the target Lean/Mathlib pins.
• @Paul-Lez has another Comparator integration in progress, so treat this one as a reference implementation for now. When his is ready, we'll compare/consolidate into a final PR.

A couple findings from going through FC100OpenSet1:

• None of the 100 problems depends on another FC problem module. ChallengeDeps is enough for the first import, so I don't think general multi-file Challenge support needs to block FC100 (dependency breakdown is in the PR body).
• One open question is where the type for an answer(sorry) slot should become authoritative. Right now the importer reads it from FC's elaborated environment, but the generated problem is ultimately built under LeanEval's pins.

My guess is the importer should carry the source declaration/provenance across, and LeanEval should validate or re-resolve the answer slot under its own target environment. Does that match what you had in mind for the split?

[kim-em]

The implementation program for this overhaul is now available as a public gist: https://gist.github.com/kim-em/cd6ac1c049f459ef9aa37d6cf551d9e4

It incorporates the RFC discussion, the parallel-agent work breakdown, migration and rollout gates, automatic Cloudflare deployment plus infrastructure documentation, and the follow-up security review of replay/release key handling.

[kim-em]

Plan correction applied to the public implementation-program gist: private replay is now explicitly a dedicated, provider-neutral LeanEval boundary with no dependency on chonk or any other project runner. D6 now records the selected dedicated AWS/KMS bootstrap behind a portable wrap/unwrap interface, with provider-loss recovery out of scope. The unrequested recovery/rollback drill requirements were removed in favor of concise procedures and ordinary health smoke checks. The gist URL is unchanged: https://gist.github.com/kim-em/cd6ac1c049f459ef9aa37d6cf551d9e4

[kim-em]

Terminology correction for the implementation program: unqualified v1 and v2 now refer only to problem sets. The current platform work is the lifecycle overhaul, and the resulting system/UI is lifecycle-aware. Machine formats are written explicitly as, for example, results schema version 2; frozen paths and identifiers such as results-v2 remain unchanged.

This rule is now recorded in the plan and public gist, and the repository wording update merged in #554.

[kim-em]

Lifecycle-overhaul implementation is at three explicit independent-review lanes; all listed heads are green. Reviewer selection is left to the maintainers—no individual review requests are assigned by this implementation work.

1. Generator/consumer: generator #1 → #2 → #3, then finalize the upstream pin in lean-eval #553.
2. Security/runtime: independently review submissions #1207 and especially the AWS key-adapter/staging-smoke boundary in #1208. No AWS authority is connected yet.
3. Release tooling: terminology prerequisite releases #3, then planner #1, then reconstruction #2.

These review gates will not be bypassed. Leaderboard #72 remains a separate stakeholder-visual-review hold; production intake and D7 remain held. The live replay-staging ref-policy correction and infrastructure-ledger update are complete in submissions #1233.

[kim-em]

D7 is complete. Maintainer-approved dry run 32569220655 fixed the exact source commit/digest, 1,298-record count, and canonical output digest; guarded apply run 32569936026 produced results-store commit c3491661. Independent post-apply checks found 44/44 schema-version-2 files, 1,298/1,298 records, no duplicates, no remaining rewrite, no writer lock, no queued submission writer, and green main CI. The tracker/ledger update merged in submissions #1241. Production intake remains disabled.