Prefer the separate editorially reviewed prompts and reviewed references for the reviewed subset. Review is AI editorial checking, not full Lean verification.

Public questions and answers may already occur in training data. This is not an unseen test set, a model ranking, or evidence that a paper is fully formalized.

Numbered textbook exercises and our reference solutions

The Bench must include actual source-pinned textbook exercises as well as original library-grounded QA. Each needs the original number and edition, a license-compliant complete statement, our stepwise formula answer, independent review and exact compiled Lean/graph links. Partial solutions stay partial; alternative valid proofs receive credit.

Browse numbered textbook exercises

Verified source intake and admission checklist · Existing Chewi Optimization Exercise 3.2 source/solution window.

Intake itself is not admission, an aligned Lean QA or proof that all exercises are complete. Per-question review and named owned-answer build state appear separately in the directory. This does not substitute for Log-Concave Sampling, the cited Statistical Optimal Transport route or the other seven-domain material. Original QA is never relabelled as an original-book exercise.

Evaluation policy and contribution guide

29 mathematical cores and 7 graph tasks have current content-bound AI editorial acceptance. This is not full Lean coverage or empirical calibration.

Each pair shares one core, family and public-dev split. Score the two tracks separately. Human-assessed natural-language rubrics have four one-point criteria; no automated semantic grader is claimed.

Lean compiler acceptance certifies the fixed proposition only. Arbitrary model output requires target-preservation checks and an isolated, resource-limited sandbox. No submission execution service or AI API is connected here.

Only original or permission-cleared material may enter ML training/evaluation. Restricted external indexes and their derivatives are excluded. Each question discloses its current editorial status and remaining formal boundary; compilation is not that review. Future drafts require their own review.

Commands, grading protocol and how to add a core · License boundaries