Reviewing

Managing pull request branches

Currently the pi-Base automatically compiles a preview of each branch on the pi-base/data repository. This does not include branches opened on forks of the repository (to prevent compiling untrusted data which could have unwanted or illegal content). So after a pull request is seen to be legitimate, a reviewer may duplicate the content of a pull request to a new branch via these steps.

First, use GitHub.dev to open the pull request.

Then use the bottom toolbar to create a new branch based on the PR.

Back at github.com you can see the new branch and confirm it compiled.

You can now also use the new branch name you created to preview the pull request at https://topology.pi-base.org/dev

At this point, you can approve and merge the original pull request, request that the contributor make changes to their pull request, or close their pull request and re-open a new pull request with the branch owned by pi-base to continue the contribution there (where it will be built and previewed).

Reviewing Checklist

The golden rules:

• New volunteers should be especially encouraged and thanked for their contributions.
• Contributions that add verifiable mathematical knowledge to the pi-Base with appropriate references should be merged as soon as possible.
  • If the PR could nonetheless could be improved (e.g. a better choice of naming, a more useful description), those improvements should be proposed in a separate issue/PR (whether by encouraging the original contributor, or directly by the reviewer).
  • If the result is not directly addressed by a source, it can be proven in the description provided that the proof is immediate. Otherwise, opening a Q&A on e.g. Math.StackExchange is likely appropriate (and that mathse reference should be used on $\pi$-Base).
• If minor errors (e.g. typos) are found, the reviewer can edit the PR directly before accepting and merging the PR.

Contributions that edit/add a "trait" (pair of an existing space/property) are typically acceptable unless the trait is already deduced by existing theorems.

Since there are infinitely-many possible spaces and properties, the introduction of new spaces and properties have a higher bar to meet. Likewise, we have some requirements on new theorems in order to ensure high-quality automated deductions.

Requirements for a new property

• The property should be of interest to researchers, whether it appears in the peer-reviewed literature or another scholarly venue such as MathOverflow.
• If the definition of a property depends on other properties, they should be cited using {Pxyz} in the description, assuming they exist. If they don't exist, these other properties should be added before or alongside the new property.
• The contribution should also include added traits and/or theorems that allows the pi-Base to deduce whether or not this property holds for multiple spaces (or there should be plans to do so in future contributions).

Requirements for a new space

At least one of the folowing should be satisfied.

• The space is of interest to researchers, preferably appearing in a textbook or the peer-reviewed literature.
• The space provides an example/counter-example that is not currently represented in the pi-Base (e.g. it is a space that is X and Y but not Z, and the pi-Base does not already know of such an example). So the contribution should include sufficient traits/theorems to provide this.
• The space provides a convenient characterization of another space (e.g. S199 was introduced to define S44 as a product).

Requirements for a new theorem

• The thoerem should be of the form AND(list of props) => prop.
  • Tip: a theorem of the form P or Q => R can be split into two theorems P => R and Q => R. Likewise P => Q or R and be rewritten as P and ~Q => R, and so on.
• The theorem should not be deducible from existing theorems.
  • Tip: if the theorem P and Q => R can be deduced, a search for P and Q and ~R in pi-Base will point this out.
• If a new theorem makes other theorems redundant, consider whether the other theorems should instead be edited to be generalized.
• We like for theorems to be generalized when possible (e.g. assume regular, not $T_3$). But this should be considered on balance with usage in the literature (if the result is only cared about in the context of "assume all spaces are Hausdorff", then it's fine to have the technically weaker result).
  • Put another way, it's okay to accept a contribution of "$T_3$ and P implies Q" even when the result could be improved to "regular and P implies Q". But this does not mean we should reject a later improvement of the result to say "regular and P implies Q" if a contributor suggests doing so.