Skip to content

No labels!

There aren’t any labels for this repository quite yet.

62 labels

Sort
Sort
Alphabetically
Reverse alphabetically
Most issues
Fewest issues
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
239
awaiting-CI
awaiting-CI
36
awaiting-review-DONT-USE
awaiting-review-DONT-USE
Read the "Changes to the #queue" announcement on Zulip
awaiting-zulip
awaiting-zulip
There is a Zulip discussion; the author should await and report/implement the decision reached there
6
blocked-by-batt-PR
blocked-by-batt-PR
This PR depends on a PR to Batteries
2
blocked-by-core-PR
blocked-by-core-PR
This PR depends on a PR to Core/Std
1
blocked-by-core-release
blocked-by-core-release
Not relevant for the current Lean release candidate, but will be needed for the next.
1
blocked-by-other-PR
blocked-by-other-PR
This PR depends on another PR to Mathlib (this label is automatically managed by a bot)
175
blocked-by-qq-PR
blocked-by-qq-PR
This PR depends on a PR to Quote4
bug
bug
Something isn't working
6
CI
CI
Modifies the continuous integration / deployment setup
14
closed-due-to-inactivity
closed-due-to-inactivity
Inactive PR (unclear if adoption would be valuable)
delegated
delegated
21
dependency-bump
dependency-bump
This PR bumps the version of an upstream dependency (but not toolchain).
1
documentation
documentation
Improvements or additions to documentation
11
easy
easy
< 20s of review time. See the lifecycle page for guidelines.
9
enhancement
enhancement
New feature or request
19
FLT
FLT
part of the ongoing formalization of Fermat's Last Theorem
3
good first issue
good first issue
Good for newcomers
10
help-wanted
help-wanted
The author needs attention to resolve issues
24
IMO
IMO
Math olympiad problems
3
lean4-change-in-behaviour
lean4-change-in-behaviour
Describes a known change in behaviour. No implication that it "needs fixing".
11
lftcm2024
lftcm2024
This PR is part of a project done during LFTCM2024
longest-pole
longest-pole
This PR aims to reduce the longest pole in Mathlib
maintainer-merge
maintainer-merge
13
mathlib3-pair
mathlib3-pair
This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged
mathlib-port
mathlib-port
This is a port of a theory file from mathlib.
1
merge-conflict
merge-conflict
The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
487
modifies-tactic-syntax
modifies-tactic-syntax
This PR adds a new interactive tactic or modifies the syntax of an existing tactic.
5