diff --git a/templates/contribute/how-to-contribute.md b/templates/contribute/how-to-contribute.md index ed8cc8558..7dafb4083 100644 --- a/templates/contribute/how-to-contribute.md +++ b/templates/contribute/how-to-contribute.md @@ -112,6 +112,7 @@ However, anyone can add/remove the labels below by writing the following command - `easy` will add the **"easy"** label - `-easy` will remove the **"easy"** label - `help-wanted`, `-help-wanted`, `please-adopt`, `-please-adopt` can be used to mark a PR in need of external input. +- `LLM-generated`, `-LLM-generated` should be used to mark a PR containing a substantial amount of LLM-generated code. (Remember that if you used AI, you must explain the specifics in the PR description.) - The labels for use by contributors upstreaming work from the downstream projects **brownian**, **carleson**, **CFT**, **FLT**, **infinity-cosmos**, **sphere-packing** and **toric** can be added and removed in the same way. - Any topic label of the form `t-*` (e.g. `t-topology`), as well as the labels `CI` and `IMO`, can also be added and removed in the same way. PRs are auto-labeled based on their contents, but sometimes the auto-labeling is incorrect or incomplete so this lets you manually override it. See [available topic labels](https://github.com/leanprover-community/mathlib4/labels?q=t-).