Repository navigation
Conversation
…butions for IMO 2026
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
…/32 runs. Co-authored-by: Cursor <cursoragent@cursor.com>
…ory items. Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter imo2026, so every commit of humanfia/imo2026 is reachable here with its files under imo2026/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter ioi2026, so every commit of humanfia/ioi2026 is reachable here with its files under ioi2026/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter ipho2026, so every commit of humanfia/ipho2026 is reachable here with its files under ipho2026/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter ibo2024, so every commit of humanfia/ibo2024 is reachable here with its files under ibo2024/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter chemlib, so every commit of humanfia/chemlib is reachable here with its files under chemlib/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter lean-qit-qlg, so every commit of humanfia/lean-qit-qlg is reachable here with its files under lean-qit-qlg/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Imported with git filter-repo --to-subdirectory-filter icho2026, so every commit of humanfia/icho2026 is reachable here with its files under icho2026/. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Drop the repeated RSI Effort note from each README (the root README states it once), link sibling competitions by subdirectory, move clone instructions and the chemlib Lake dependency to humanfia/hoa-qed, and fix humanize2 links. The README lines in putnambench/MANIFEST.sha256 and ioi2026/MANIFEST.sha256, and ibo2024's canonical README hash, were already stale before this change; they now match the edited READMEs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The root README introduces HOA once, summarizes every result with a link to its directory and write-up, and keeps each project's caveats. Code and Lean proofs are Apache-2.0, prose is CC-BY-4.0, and NOTICE lists the third-party material that keeps its owner's terms. CI has two workflows. Check verifies relative Markdown links, each project's integrity manifests and its offline verifiers. Lean builds the Lake projects whose files changed, with the Mathlib cache; it replaces chemlib's own lean.yml, which no longer runs from a subdirectory. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The project ships no lake-manifest.json, which lean-action requires. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
imo2026/base declares lean_lib MathFlowBench without a MathFlowBench.lean root (the run harness writes one into each workspace), so a bare lake build reports bad imports. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
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
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.
Turns
humanfia/hoa-qedinto the HOA monorepo. The PutnamBench release moves intoputnambench/, and seven other repositories join it, each with its full history.What changes
putnambench/is agit mvof the existing root, so its history is this repository's own.imo2026,ioi2026,ipho2026,icho2026,ibo2024,chemlibandlean-qit-qlgwere rewritten withgit filter-repo --to-subdirectory-filter <name>and merged with--allow-unrelated-histories. Every source commit is kept, sogit log -- <dir>andgit blamework per directory. Commit hashes in those histories are new; the one hash a README cited (IOI provenanceb1c4c8bd…) now gives its monorepo equivalent too.humanfia/hoa-qed(subDir = "chemlib/chemlib"), andhumanize2links are fixed. Instructions that said "repository root" now name the subdirectory.README.mdlines inputnambench/MANIFEST.sha256andioi2026/MANIFEST.sha256, and the canonical README hash inibo2024/scripts/validate.py, were already stale on the source repos. They now match the edited READMEs. No solution or proof hash changed.LICENSE(Apache-2.0),LICENSE-CC-BY-4.0for prose,NOTICEfor third-party material,CITATION.cff,.github/CODEOWNERSanddependabot.ymlfor Actions.check.ymlchecks relative Markdown links, runsputnambench/reproduce.sh checkandioi2026/verify.sh, checks the IChO checksums and the IBO solution manifest, and runsibo2024/scripts/build.py --check.lean.ymlbuilds each changed Lake project with the Mathlib cache (10 projects, path-filtered; a manual run builds all of them). It replaceschemlib/.github/workflows/lean.yml, which would not run from a subdirectory. Every action is pinned to a full commit SHA.Not covered
imo2026/basedeclareslean_lib MathFlowBenchwith noMathFlowBench.leanroot, because the run harness writes one into each workspace. A barelake buildthere fails with "bad imports", as the README's instructions already did. CI buildsMathFlowBench.CacheWarmand then checks all 12 solution files withlake env lean.icho2026/*-native-goal68/jobs/are not built in CI.putnambench/humanize/is a vendored snapshot ofPolyArch/humanize, which declares no license. NOTICE says it stays under that project's terms.🤖 Generated with Claude Code