Labels

PRs resulting from the ICERM Workshop on Autoformalization 24/04/25-27/04/25

Math olympiad problems

Automatically added label for PRs which increase "strong" technical debts

This PR is associated with Infinity Cosmos project

Automatically added label for PRs with a significant increase in transitive imports

Describes a known change in behaviour. No implication that it "needs fixing".

This PR contains material coming from the Lean Machine Learning library.

This PR is part of a project done during LFTCM2024

PRs with substantial input from LLMs - review accordingly

This PR aims to reduce the longest pole in Mathlib

A reviewer has approved the changed; awaiting maintainer approval.

This is a port of a theory file from mathlib.

This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged

The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

This PR may have important context in comments on the old PR.

This PR adds a new interactive tactic or modifies the syntax of an existing tactic.

This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!

Something that improves performance but is poorly understood.

landrun failed during CI

Inactive PR (would be valuable to adopt)

We've changed something in the CI setup!

Mathlib3 to Mathlib4 porting notes.

This PR has been sent to bors.

Request for comment

Material from https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean

Algebra (groups, rings, fields, etc)

Algebraic geometry