From 7526628c816cda2d2ed5f20142f33c0168f01a58 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 12:02:43 +0100 Subject: [PATCH 1/4] Create ReviewChecklist.md --- docs/ReviewChecklist.md | 47 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 docs/ReviewChecklist.md diff --git a/docs/ReviewChecklist.md b/docs/ReviewChecklist.md new file mode 100644 index 000000000..bd00bdda1 --- /dev/null +++ b/docs/ReviewChecklist.md @@ -0,0 +1,47 @@ +# Review checklist + +This is a review checklist for Lean content going into ./Physlib or ./QuantumInfo. +It does not cover meta-programs, only standard additions of definitions and lemmas to Lean. + +This should not be taken as a definitive guide, as every PR will be different. + +There is some subjectivity in reviewing PRs, so instead of framing this in terms of hard-set rules, +this review check list is framed in terms of questions a reviewer might want to ask themsevles +when reviewing a PR. + +## Level 1: Subject area + +- Is the content added physics? +- Is the content added mainstream physics? + +## Level 2: Organisation + +- For every definition and lemma added in the PR, could I determine from the file-structure only + where I would find that result? +- Does every definition and lemma added in the PR fit the theme of the rest of the file, or + does it fit more appropriately elsewhere? +- If there are new files made, can I guess the content of that file from the name? +- Within a given file, can I understand the relevence of results which sit next to each other, + or in the same section? + +## Level 3: Content + +- Is a definition or lemma a simple rewrite of a result already in Mathlib or Physlib? +- Do the definitions added look generally useful, do they appear in physics, or + do they allow you to ask interesting questions about a data-structure that exists? +- Are lemma statements and definition terms easy to read? +- Do lemmas seem like they will be useful, and are written in a reusable way? + +## Level 4: Naming and documentation + +- Are the names written in Mathlib/Physlib convention? +- From the name of a declaration can you guess what the declaration is without looking at it? +- Are the namespaces correct and make sense? +- Does the module documentation actually help either with the flow of the document or one + understand what is in the file, or is it just padding? +- Does documentation on declrations help one understand what that decleration does? + +## Level 5: + +- Does the code look neat and clean, or is it difficult to read? +- Are there any newlines in proofs? From eda2611034d1481c34dde66f311863ac25f80cc6 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 13:00:19 +0100 Subject: [PATCH 2/4] Update docs/ReviewChecklist.md Co-authored-by: nateabr <135662056+nateabr@users.noreply.github.com> --- docs/ReviewChecklist.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/ReviewChecklist.md b/docs/ReviewChecklist.md index bd00bdda1..037cb097a 100644 --- a/docs/ReviewChecklist.md +++ b/docs/ReviewChecklist.md @@ -31,7 +31,7 @@ when reviewing a PR. do they allow you to ask interesting questions about a data-structure that exists? - Are lemma statements and definition terms easy to read? - Do lemmas seem like they will be useful, and are written in a reusable way? - +Are the hypotheses of the lemma minimal and necessary? ## Level 4: Naming and documentation - Are the names written in Mathlib/Physlib convention? From df0036f723ad0e62dbf921839ad1edc63931bea7 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 13:01:19 +0100 Subject: [PATCH 3/4] refactor: Added suggestions Co-Authored-By: nateabr <135662056+nateabr@users.noreply.github.com> --- docs/ReviewChecklist.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/ReviewChecklist.md b/docs/ReviewChecklist.md index 037cb097a..e4bf63dff 100644 --- a/docs/ReviewChecklist.md +++ b/docs/ReviewChecklist.md @@ -31,7 +31,10 @@ when reviewing a PR. do they allow you to ask interesting questions about a data-structure that exists? - Are lemma statements and definition terms easy to read? - Do lemmas seem like they will be useful, and are written in a reusable way? -Are the hypotheses of the lemma minimal and necessary? +- Are the hypotheses of the lemma minimal and necessary? +- Do any of the have statements inside the proof contain general mathematical identities or + physical context that should be extracted into their own standalone lemmas? + ## Level 4: Naming and documentation - Are the names written in Mathlib/Physlib convention? From 69a5a33f635821b8b8ffab2c1bc1fda6af13b858 Mon Sep 17 00:00:00 2001 From: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 3 Jul 2026 13:02:23 +0100 Subject: [PATCH 4/4] fix: Spelling --- docs/ReviewChecklist.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/ReviewChecklist.md b/docs/ReviewChecklist.md index e4bf63dff..985e076e4 100644 --- a/docs/ReviewChecklist.md +++ b/docs/ReviewChecklist.md @@ -21,7 +21,7 @@ when reviewing a PR. - Does every definition and lemma added in the PR fit the theme of the rest of the file, or does it fit more appropriately elsewhere? - If there are new files made, can I guess the content of that file from the name? -- Within a given file, can I understand the relevence of results which sit next to each other, +- Within a given file, can I understand the relevance of results which sit next to each other, or in the same section? ## Level 3: Content @@ -42,7 +42,7 @@ when reviewing a PR. - Are the namespaces correct and make sense? - Does the module documentation actually help either with the flow of the document or one understand what is in the file, or is it just padding? -- Does documentation on declrations help one understand what that decleration does? +- Does documentation on declarations help one understand what that declaration does? ## Level 5: