Labels

• auto-merge-after-CI

  auto-merge-after-CI

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

• awaiting-author

  awaiting-author

  A reviewer has asked the author a question or requested changes.

• awaiting-bench

  awaiting-bench

  This PR needs to be benchmarked before merging

• awaiting-CI

  awaiting-CI

  This PR does not pass CI yet. This label is automatically removed once it does.

• awaiting-requeue

  awaiting-requeue

  This PR was on the bors queue but came off after a build failure or other issue.

• awaiting-zulip

  awaiting-zulip

  There is a Zulip discussion; the author should await and report/implement the decision reached there

• blocked-by-batt-PR

  blocked-by-batt-PR

  This PR depends on a PR to Batteries

• blocked-by-core-PR

  blocked-by-core-PR

  This PR depends on a PR to Core/Std

• blocked-by-core-release

  blocked-by-core-release

  Not relevant for the current Lean release candidate, but will be needed for the next.

• blocked-by-other-PR

  blocked-by-other-PR

  This PR depends on another PR (this label is automatically managed by a bot)

• blocked-by-qq-PR

  blocked-by-qq-PR

  This PR depends on a PR to Quote4

• bors-staging

  bors-staging

  This PR is currently being built by bors on the staging branch.

• brownian

  brownian

  Part of the ongoing formalization of the Brownian motion and stochastic integrals

• bug

  bug

  Something is not working

• carleson

  carleson

  part of the ongoing formalization of Carleson's theorem

• CFT

  CFT

  Part of the ongoing formalisation of class field theory

• CI

  CI

  Modifies the continuous integration setup or other automation

• closed-due-to-inactivity

  closed-due-to-inactivity

  Inactive PR (unclear if adoption would be valuable)

• codex

  codex

  OpenAI Codex wrote (parts of) this PR.

• delegated

  delegated

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

• dependencies

  dependencies

  Pull requests that update a dependency file

• dependency-bump

  dependency-bump

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

• documentation

  documentation

  Improvements or additions to documentation

• easy

  easy

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

• enhancement

  enhancement

  New feature or request

• file-removed

  file-removed

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

• FLT

  FLT

  part of the ongoing formalization of Fermat's Last Theorem

• github_actions

  github_actions

  Pull requests that update GitHub Actions code

• good first issue

  good first issue

  Good for newcomers

• help-wanted

  help-wanted

  The author needs attention to resolve issues