Skip to content

Labels

Labels

  • area:ci

    GitHub Actions, Docker images, build gates, and release automation
  • area:docs

    Markdown docs, onboarding, coverage prose, and cross-links
  • area:identification

    Identification/ — potential outcomes, designs, and what pins an estimand down
  • area:tooling

    Verification tools, scripts, ledger logic, and generated audits
  • autoform

    opened by the autoform pipeline; review before merge
  • bug

    Something isn't working
  • difficulty:good-first

    Small, well-scoped task for new contributors
  • difficulty:hard

    Requires deep domain knowledge or upstream coordination
  • difficulty:medium

    Requires repo context, Lean fluency, or careful validation
  • difficulty:small

    Straightforward change for someone familiar with the repo
  • documentation

    Improvements or additions to documentation
  • duplicate

    This issue or pull request already exists
  • enhancement

    New feature or request
  • good first issue

    Good for newcomers
  • help wanted

    Extra attention is needed
  • invalid

    This doesn't seem right
  • question

    Further information is requested
  • status:blocked-design

    Blocked on a modeling, theorem-shape, or architecture decision
  • status:blocked-upstream

    Blocked on Mathlib or another external project
  • status:in-progress

    Someone is actively working on it
  • status:needs-info

    Waiting on clarification before work should start
  • status:needs-triage

    New issue that has not been classified yet
  • status:ready

    Scoped enough for a contributor to pick up
  • status:review

    PR exists and maintainer review is the next step
  • type:bug

    Something expected to work is broken
  • type:docs

    Documentation-only work
  • type:maintenance

    Routine cleanup, dependency updates, or housekeeping
  • type:proof

    Lean theorem, proof repair, or theorem generalization
  • type:refactor

    Structure or naming change that should preserve behavior
  • type:research

    Open investigation where the path is not yet clear