Add a lakefile for the LEAP Lean solutions - #17
Open
Vilin97 wants to merge 1 commit into
Open
Conversation
Pins Lean/mathlib v4.21.0 (the toolchain of AxiomMath/putnam2025, which these solutions target). With it, 'lake exe cache get && lake build' compiles 31 of the 58 solution files out of the box, including the Putnam 2025 set; the remaining files appear to target a different mathlib vintage. This makes the corpus mechanically checkable rather than read-only.
Vilin97
added a commit
to Vilin97/lean-code-reuse
that referenced
this pull request
Jul 20, 2026
…3) removed - Erdos90's src/submission ships its own lakefile (v4.30.0): full 2h40m build, exact tier with 37k decls / 2.6M edges. - Seed-Prover's imo2025 subproject ships a lakefile (v4.14.0, confirming the README); built and used as a tier-validation slice: textual vs exact Spearman 0.975 on the dump genre — the textual tier is essentially exact there. - Authored leap/lakefile.lean for google-deepmind/superhuman (v4.21.0, 31/58 files compile; corpus mixes mathlib vintages) and opened upstream PR google-deepmind/superhuman#17. - Rubik Cube Group removed from the corpus (predominantly Lean 3). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011pxj7RaxUiRdq8SmQm3iKg
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The
leap/solutionscorpus currently ships as standalone.leanfiles with no build configuration, so verifying that the proofs compile requires manual setup.This PR adds a minimal
lakefile.lean+lean-toolchain(and a.gitignorefor lake artifacts) pinning Lean/mathlib v4.21.0 — the toolchain of AxiomMath/putnam2025, which the Putnam solutions target. With it:compiles 31 of the 58 solution files out of the box, including the Putnam 2025 set. The remaining files (mostly under
LEAN-IMO-Bench) appear to target a different mathlib vintage — e.g. they referenceFinset.card_sdiff_of_subset, which does not exist in v4.21 — so a per-directory pin (or a note of the intended versions) would be needed to make the whole corpus checkable; happy to adjust if the team can share the versions used.Motivation: we've been measuring structural quality metrics across Lean corpora (reuse graphs, hygiene, elaboration cost — https://vilin97.github.io/lean-code-reuse/), and machine-checkability of published proof corpora is the first gate for any such analysis.
🤖 Generated with Claude Code
https://claude.ai/code/session_011pxj7RaxUiRdq8SmQm3iKg