lean-eval submissions

Solved lean-eval benchmark workspaces, one per subdirectory.

This repository is a submission source, not the submission target. To score these on the public leaderboard, open a "Submit benchmark solution" issue on leanprover/lean-eval-submissions and point its Submission URL at this repo. That CI walks every subdirectory, finds each lakefile.toml whose name matches a benchmark problem id with a Submission.lean alongside, and scores it with the comparator. Only Submission.lean and files under Submission/ are ever read.

Problems

Problem	Status	Model
baer_suzuki	✅ comparator-accepted (local lake test)	Claude Opus 4.7 + GPT-5.5 (human-in-the-loop)

Layout

Each <problem>/ is a self-contained comparator workspace generated from leanprover/lean-eval:

• Submission.lean, Submission/ — the solution (solver-owned)
• Challenge.lean, Solution.lean, ChallengeDeps.lean, config.json, lakefile.toml, … — trusted scaffold, identical to the benchmark's generated/<problem>/

Local check

cd <problem>
lake test

Requires the comparator toolchain (comparator, landrun, lean4export) on PATH; see the lean-eval README.