A reviewer has asked the author a question or requested changes
The author would like to see what CI has to say before doing more work.
The author would like community review of the PR
This PR depends on another PR which is still in the queue. A bot manages this label via PR comment.
The #outofsync queue must have at most 20 items
This issue or PR is about continuous integration
The PR author may merge after reviewing final suggestions.
This PR is about documentation
< 20s of review time. See the lifecycle page for guidelines.
This issue is a feature request, either for mathematics, tactics, or CI
Without this label hacktoberfest is scared off by bors
The author needs attention to resolve issues
Formalisation of an IMO problem
Co-authored by `lean-gptf`
This PR only fixes linting errors
This PR *only* adds a message to the module doc about synchronization with mathlib4
For compatibility with Lean 4 changes, to simplify porting
Please `git merge origin/master` then a bot will remove this label.
This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.