# Description
Motivated by [this
comment](#3804 (comment)),
adding a bit documentation on our custom label creation (without
elevated rights on the repo).

# Testing
No-op change.

# Description
Motivated by [this
comment](#3804 (comment)),
we would like to harmonize the AMS tags in the repo and disallow leading
zeros:
- Raise linting warning if the AMS tag contains leading zeros
- Fix 17 existing files not following the new convention

# Testing
:white_check_mark: Built the whole repo successfully without linting
warnings
```shell
$ lake build
Build completed successfully (8669 jobs).
```

# Description
> If $A \subset \mathbb{Z}/p\mathbb{Z}$ is random, $|A| = \sqrt{p}$, can
we almost surely cover $\mathbb{Z}/p\mathbb{Z}$ with $100\sqrt{p}$
translates of $A$?

- Closes google-deepmind#1595
- 🤖 First draft created with help from **Gemini 3.1 Pro**. I then
modified it to handle edge cases, improved code modularity, added
variants, and simple tests. I then asked Gemini to come up with
non-trivial tests by enumeration.
- Formulation handles the 3 problem variants mentioned in Green's
original comments.

# Testing
✅ Builds successfully
```shell
$ lake build FormalConjectures/GreensOpenProblems/39.lean 
Build completed successfully (7982 jobs).
```

…pmind#3934)

# Description
Motivated by [this
comment](google-deepmind#3804 (comment)),
adding a bit documentation on our custom label creation (without
elevated rights on the repo).

# Testing
No-op change.

…#3933)

# Description
Motivated by [this
comment](google-deepmind#3804 (comment)),
we would like to harmonize the AMS tags in the repo and disallow leading
zeros:
- Raise linting warning if the AMS tag contains leading zeros
- Fix 17 existing files not following the new convention

# Testing
:white_check_mark: Built the whole repo successfully without linting
warnings
```shell
$ lake build
Build completed successfully (8669 jobs).
```