Labels

• assumption

  A result from the 1980s or before which is not currently being worked on and which will be assumed.
• auto-update-lean
• auto-update-lean-fail

  Auto update for Lean dependencies
• awaiting-author
• awaiting-CI
• awaiting-merge
• awaiting-review
• Big Proof

  Issues that should be dealt with before Big Proof
• dependencies

  Pull requests that update a dependency file
• do-not-merge
• documentation

  Improvements or additions to documentation
• github_actions

  Pull requests that update GitHub Actions code
• good first issue

  Good for newcomers
• help wanted

  Extra attention is needed
• infrastructure

  Modification or update of tooling for QA, installation, CI or deployment
• MVP

  Required for the delivery of a minimum viable product
• on hold

  Waiting for more information or something else to happen
• optimisation

  Improvements in the performance of the code
• question

  Further information is requested
• refactor

  Refactoring existing code without significantly changing functionality
• reference-only

  This PR will not be merged; it is just older work which may serve as a useful reference
• ruby

  Pull requests that update Ruby code
• straightforward

  This task should hopefully be doable in one sitting if you know the relevant part of mathlib.
• task
• umbrella

  To group together multiple interrelated issues and track their progress
• upstream

  An bug or feature that needs sorting in a dependency
• WIP
• wontfix

  This will not be worked on