From 5e1d39a5bd32ab3056576f8ce858bde11ebcfb77 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Thu, 2 Jul 2026 18:11:10 -0400 Subject: [PATCH 1/4] doc(ErdosProblems/README): add a before-requesting-review checklist --- FormalConjectures/ErdosProblems/README.md | 25 +++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/FormalConjectures/ErdosProblems/README.md b/FormalConjectures/ErdosProblems/README.md index a501829897..fd9c4afe12 100644 --- a/FormalConjectures/ErdosProblems/README.md +++ b/FormalConjectures/ErdosProblems/README.md @@ -48,3 +48,28 @@ An example of this would be: - [Va99] Various, Some of Paul's favorite problems. Booklet produced for the conference "Paul Erdős and his mathematics", Budapest, July 1999 (1999). ``` + +## Before requesting review + +A checklist of the corrections that come up most often in review. Ticking +these off first (yourself, or whatever agent prepared the PR) usually saves a +review round trip: + +1. **Docstrings quote the website verbatim.** Copy the LaTeX from + erdosproblems.com rather than rephrasing it. Only deviate to fix a genuine + error or inaccuracy in the original formulation. +2. **Solved problems cite the solution.** The text below the problem box + typically explains who solved it and in which paper; copy that sentence + verbatim into the docstring as well. +3. **Search before defining.** Check `FormalConjecturesForMathlib` and + neighboring problem files for existing definitions, API, and notation + before introducing your own. If something you need seems generally useful, + it belongs in `FormalConjecturesForMathlib`, not inlined in the problem + file. +4. **Keep commentary out of the Lean file.** Notes to reviewers, formalization + choices, and caveats belong in the pull request description, not the + source. +5. **Use LaTeX, not backticks, for mathematics in docstrings.** See + `AGENTS.md` for the exceptions on the Lean-API side. +6. **Add sanity tests for new definitions.** A nontrivial definition should + come with at least one `@[category test]` statement exercising it. From 9feae26c140d0b89afa0f4b7ab24a72326a0469d Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Fri, 3 Jul 2026 14:55:42 -0400 Subject: [PATCH 2/4] doc: author checklist as a PR template + the two missing AGENTS.md rules --- .github/PULL_REQUEST_TEMPLATE.md | 11 +++++++++++ AGENTS.md | 4 ++++ 2 files changed, 15 insertions(+) create mode 100644 .github/PULL_REQUEST_TEMPLATE.md diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 0000000000..28fc6fc929 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -0,0 +1,11 @@ + + +--- + +- [ ] I checked `AGENTS.md` and the README of the directory I'm contributing to (e.g. `FormalConjectures/ErdosProblems/README.md`) +- [ ] Every result carries a `@[category ...]` and an `@[AMS ...]` attribute +- [ ] Docstrings quote the source verbatim, with references in the module docstring +- [ ] I searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding my own +- [ ] New definitions or attribute behavior come with `@[category test]` / demo tests +- [ ] `lake --wfail build` passes locally diff --git a/AGENTS.md b/AGENTS.md index a9d0e97508..f4b602979b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -461,6 +461,8 @@ Before considering your work complete, verify: - [ ] Docstrings present for main definitions - [ ] `research open`, `textbook` and `research solved` docstrings include a concise description - [ ] Code properly formatted and readable +- [ ] Searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones +- [ ] Notes to reviewers (formalization choices, caveats) are in the PR description, not the Lean file ### Testing Definitions @@ -490,6 +492,8 @@ theorem myNewClass_sanity_check : - Add large proofs (this is a benchmark repository, not a proof repository) - Use camelCase for theorem names - Create placeholder definitions in FormalConjecturesForMathlib/ +- Redefine notation or API that already exists in `FormalConjecturesForMathlib` or a neighboring problem file +- Put meta-commentary or notes-to-reviewers in Lean files (they belong in the PR description) ✅ **DO:** From 54521f8e7bd0835d4b47fc7cb45bb10dc178d709 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Fri, 3 Jul 2026 14:58:58 -0400 Subject: [PATCH 3/4] drop the PR template; keep the checklist in AGENTS.md and the ErdosProblems README --- .github/PULL_REQUEST_TEMPLATE.md | 11 ----------- 1 file changed, 11 deletions(-) delete mode 100644 .github/PULL_REQUEST_TEMPLATE.md diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md deleted file mode 100644 index 28fc6fc929..0000000000 --- a/.github/PULL_REQUEST_TEMPLATE.md +++ /dev/null @@ -1,11 +0,0 @@ - - ---- - -- [ ] I checked `AGENTS.md` and the README of the directory I'm contributing to (e.g. `FormalConjectures/ErdosProblems/README.md`) -- [ ] Every result carries a `@[category ...]` and an `@[AMS ...]` attribute -- [ ] Docstrings quote the source verbatim, with references in the module docstring -- [ ] I searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding my own -- [ ] New definitions or attribute behavior come with `@[category test]` / demo tests -- [ ] `lake --wfail build` passes locally From 434387eea148bc081022112fb6cca3346528a0e7 Mon Sep 17 00:00:00 2001 From: Will Blair <85643015+willblair0708@users.noreply.github.com> Date: Sun, 5 Jul 2026 10:57:55 -0400 Subject: [PATCH 4/4] =?UTF-8?q?address=20review:=20apply=20mo271's=20AGENT?= =?UTF-8?q?S.md=20suggestions;=20keep=20only=20Erd=C5=91s-specific=20items?= =?UTF-8?q?=20in=20the=20README?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - AGENTS.md: search mathlib too, add 'AI support used', include mathlib in the redefine-notation pitfall (mo271's suggestions) - ErdosProblems/README: drop the general checklist items (search-before-defining, commentary-out-of-Lean, LaTeX-not-backticks, sanity-tests); they live in AGENTS.md. Keep the two erdosproblems.com-specific ones and link the general checklist. --- AGENTS.md | 6 +++--- FormalConjectures/ErdosProblems/README.md | 18 +++--------------- 2 files changed, 6 insertions(+), 18 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index f4b602979b..c279dd9fd6 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -461,8 +461,8 @@ Before considering your work complete, verify: - [ ] Docstrings present for main definitions - [ ] `research open`, `textbook` and `research solved` docstrings include a concise description - [ ] Code properly formatted and readable -- [ ] Searched `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones -- [ ] Notes to reviewers (formalization choices, caveats) are in the PR description, not the Lean file +- [ ] Searched mathlib and `FormalConjecturesForMathlib` and neighboring files for existing definitions, API, and notation before adding new ones +- [ ] Notes to reviewers (formalization choices, caveats, AI support used) are in the PR description, not the Lean file ### Testing Definitions @@ -492,7 +492,7 @@ theorem myNewClass_sanity_check : - Add large proofs (this is a benchmark repository, not a proof repository) - Use camelCase for theorem names - Create placeholder definitions in FormalConjecturesForMathlib/ -- Redefine notation or API that already exists in `FormalConjecturesForMathlib` or a neighboring problem file +- Redefine notation or API that already exists in mathlib, `FormalConjecturesForMathlib` or a neighboring problem file - Put meta-commentary or notes-to-reviewers in Lean files (they belong in the PR description) ✅ **DO:** diff --git a/FormalConjectures/ErdosProblems/README.md b/FormalConjectures/ErdosProblems/README.md index fd9c4afe12..04dbeecd68 100644 --- a/FormalConjectures/ErdosProblems/README.md +++ b/FormalConjectures/ErdosProblems/README.md @@ -51,9 +51,9 @@ An example of this would be: ## Before requesting review -A checklist of the corrections that come up most often in review. Ticking -these off first (yourself, or whatever agent prepared the PR) usually saves a -review round trip: +The general checklist lives in +[`AGENTS.md`](../../AGENTS.md#quality-checklist). Two corrections specific to +Erdős problems come up most often in review: 1. **Docstrings quote the website verbatim.** Copy the LaTeX from erdosproblems.com rather than rephrasing it. Only deviate to fix a genuine @@ -61,15 +61,3 @@ review round trip: 2. **Solved problems cite the solution.** The text below the problem box typically explains who solved it and in which paper; copy that sentence verbatim into the docstring as well. -3. **Search before defining.** Check `FormalConjecturesForMathlib` and - neighboring problem files for existing definitions, API, and notation - before introducing your own. If something you need seems generally useful, - it belongs in `FormalConjecturesForMathlib`, not inlined in the problem - file. -4. **Keep commentary out of the Lean file.** Notes to reviewers, formalization - choices, and caveats belong in the pull request description, not the - source. -5. **Use LaTeX, not backticks, for mathematics in docstrings.** See - `AGENTS.md` for the exceptions on the Lean-API side. -6. **Add sanity tests for new definitions.** A nontrivial definition should - come with at least one `@[category test]` statement exercising it.