From d26e05a5a44a710c15ed5b877eefc49be783fb32 Mon Sep 17 00:00:00 2001
From: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com>
Date: Thu, 28 May 2026 10:48:04 +0300
Subject: [PATCH] `LLM-generated` can be added with comments, take 2

---
 templates/contribute/how-to-contribute.md | 1 +
 1 file changed, 1 insertion(+)

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-).