Labels

• auto-merge-after-CI

  Please do not add manually. Requests for a bot to merge automatically once CI is done.
• awaiting-author

  A reviewer has asked the author a question or requested changes.
• awaiting-bench

  This PR needs to be benchmarked before merging
• awaiting-CI

  This PR doesn't pass CI yet. This label is automatically removed once it does.
• awaiting-zulip

  There is a Zulip discussion; the author should await and report/implement the decision reached there
• bench-after-CI

  Once the PR passes CI, comment `!bench` on the PR
• blocked-by-batt-PR

  This PR depends on a PR to Batteries
• blocked-by-core-PR

  This PR depends on a PR to Core/Std
• blocked-by-core-release

  Not relevant for the current Lean release candidate, but will be needed for the next.
• blocked-by-other-PR

  This PR depends on another PR (this label is automatically managed by a bot)
• blocked-by-qq-PR

  This PR depends on a PR to Quote4
• bug

  Something isn't working
• carleson

  part of the ongoing formalization of Carleson's theorem
• CFT

  Part of the ongoing formalisation of class field theory
• CI

  Modifies the continuous integration setup or other automation
• closed-due-to-inactivity

  Inactive PR (unclear if adoption would be valuable)
• codex

  OpenAI Codex wrote (parts of) this PR.
• delegated

  This pull request has been delegated to the PR author (or occasionally another non-maintainer).
• dependencies

  Pull requests that update a dependency file
• dependency-bump

  This PR bumps the version of an upstream dependency (but not toolchain).
• documentation

  Improvements or additions to documentation
• easy

  < 20s of review time. See the lifecycle page for guidelines.
• enhancement

  New feature or request
• file-removed

  A Lean module was (re)moved without a `deprecated_module` annotation
• FLT

  part of the ongoing formalization of Fermat's Last Theorem
• github_actions

  Pull requests that update GitHub Actions code
• good first issue

  Good for newcomers
• help-wanted

  The author needs attention to resolve issues
• icerm-autoformalization

  PRs resulting from the ICERM Workshop on Autoformalization 24/04/25-27/04/25
• IMO

  Math olympiad problems