Repository navigation
Contributing guidelines for AI
This document is for reading once at the start to calibrate; ground truth sources are at the bottom.
A new contributor generally submits to a mathbox. Mathboxes are independent sandboxes whereas main (i.e. non-mathbox) is shared.
Mathboxes are placed alphabetically in last name, first name order. The first mathbox for example:
$( Begin $[ set-mbox-sa.mm $] $)
$( Skip $[ set-main.mm $] $)
$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Mathbox for Stefan Allan
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)
<contents omitted>
$( (End of Stefan Allan's mathbox.) $)
$( End $[ set-mbox-sa.mm $] $)
There is also a contributor list near the top of set.mm (line 36) where you may want to add your (i.e. the human's) name:
Contributor list:
DA David Abernethy
SA Stefan Allan
TA Thierry Arnoux
JA Juha Arpiainen
JB Jonathan Ben-Naim
GB Gregory Bush
MC Mario Carneiro
FC Filip Cernatescu
PC Paul Chapman
<...>
Theorems of mathematical interest (in contrast to helper/utility theorems) can often go in main.
There are a few formatting things that are beyond the CI checks. They're not necessarily important or blocking but it is a bit unusual (though not unheard of) to see different formatting.
So here are some notes:
A theorem in a block and a theorem in global scope. The indentation is 2 spaces. There is generally a global indentation of 2 spaces.
rewrap will format comments so just know the text in a comment is aligned to the same column ("3" indent).
${
jarrii.1 $e |- ps $.
jarrii.2 $e |- ( ( ph -> ps ) -> ch ) $.
$( Inference associated with ~ jarri . A consequence of ~ ax-mp and
~ ax-1 . (Contributed by SN, 14-Oct-2025.) $)
jarrii $p |- ch $=
( wi a1i ax-mp ) ABFCBADGEH $.
$( $j usage 'jarrii' avoids 'ax-2'; $)
$}
$( Introduction of conjunct inside of a contradiction. Would be used in
~ elfvov1 . (Contributed by SN, 18-May-2025.) $)
intnanrt $p |- ( -. ph -> -. ( ph /\ ps ) ) $=
( wa simpl con3i ) ABCAABDE $.
(Note: $j usage comments cause a CI verification that the theorem doesn't use one or more space separated single-quoted axioms.
They are used when an axiom is saved or to justify a theorem's comment that it doesn't use an axiom.
They are rare)
A more complicated example. This shows the ability for hypotheses to be shared.
Share hypotheses because it's readable and easier to write, don't get too crazy.
If disjoint variable conditions are needed they are above the hypotheses.
When a wff is too long, it is more readable to break it at a more root parsing symbol
(not a leaf); usually that is a logical or otherwise binary symbol like ->, /\, or =.
${
sepdisj.1 $e |- ( ph -> J e. Top ) $.
${
sepdisj.2 $e |- ( ph -> S C_ U. J ) $.
sepdisj.3 $e |- ( ph -> ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) $.
$( Separated sets are disjoint. Note that in general separatedness also
requires ` T C_ U. J ` and ` ( S i^i ( ( cls `` J ) `` T ) ) = (/) `
as well but they are unnecessary here. (Contributed by Zhi Wang,
7-Sep-2024.) $)
sepdisj $p |- ( ph -> ( S i^i T ) = (/) ) $=
( ccl cfv ctop wcel cuni wss eqid sscls syl2anc ssdisjd ) ABBDHIIZCADJK
BDLZMBRMEFBDSSNOPGQ $.
$}
${
$d J m n $. $d S m n $. $d T m n $.
seposep.2 $e |- ( ph -> E. n e. J E. m e. J
( S C_ n /\ T C_ m /\ ( n i^i m ) = (/) ) ) $.
$( If two sets are separated by (open) neighborhoods, then they are
separated subsets of the underlying set. Note that separatedness by
open neighborhoods is equivalent to separatedness by neighborhoods.
See ~ sepnsepo . The relationship between separatedness and closure
is also seen in ~ isnrm , ~ isnrm2 , ~ isnrm3 . (Contributed by Zhi
Wang, 7-Sep-2024.) $)
seposep $p |- ( ph -> ( ( S C_ U. J /\ T C_ U. J )
/\ ( ( S i^i ( ( cls ` J ) ` T ) ) = (/)
/\ ( ( ( cls ` J ) ` S ) i^i T ) = (/) ) ) ) $=
Double newlines are rare. Triple newlines are disallowed by CI.
Section comments do not have a global indent. In general one works with sections (a mathbox is a section) and subsections, the others are rare.
$(
###############################################################################
MAJOR PART
###############################################################################
$)
$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Section
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)
$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Subsection
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)
$(
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
Subsubsection
-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
A section comment looks like this. Lorem ipsum dolor sit amet consectetur
adipiscing elit aliqua anim expedita imperdiet dolor qui qui optio commodo.
Another paragraph. Lorem ipsum dolor sit amet consectetur adipiscing elit
aliqua anim expedita imperdiet dolor qui quotio.
$)
You can link to labels or urls using ~: ~ syl, ~ https://example.com.
Math symbols are indicated in backticks:
$( All symbols within the backticks must be defined but they don't have to
form a valid wff: ` F ( 3 sqrt 2 x y ) ` $)
Underscores can be used for italics but note that humans use italics much less than AI.
Common ending tags:
(Contributed by AN, Mmm-dd-yyyy.)(Revised by AN, Mmm-dd-yyyy.)(Proof shortened by AN, Mmm-dd-yyyy.)(Proof modification is discouraged.)(New usage is discouraged.)
where Mmm is a month like Jan and AN is either initials or the full author name.
The latter two are not line-broken and require discouraged file updating.
An AI can write (Generated by AI Name.) (Contributed by Human Name, Mmm-dd-yyyy.)
but note that this format is under discussion/not established yet.
Deduction form is preferred. Especially for theorems with a huge antecedent.
~ addcld has many more uses than ~ addcl even with the many historical non-deduction theorems that exist for basic math. A theorem with a specific antecedent is only convenient for that specific antecedent, whereas deduction theorems can be used with any antecedent.
Closed form example:
$( Alias for ~ ax-addcl , for naming consistency with ~ addcli . Use this
theorem instead of ~ ax-addcl or ~ axaddcl . (Contributed by NM,
10-Mar-2008.) $)
addcl $p |- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC ) $=
( ax-addcl ) ABC $.
Deduction form (preferred):
${
addcld.1 $e |- ( ph -> A e. CC ) $.
addcld.2 $e |- ( ph -> B e. CC ) $.
$( Closure law for addition. (Contributed by Mario Carneiro,
27-May-2016.) $)
addcld $p |- ( ph -> ( A + B ) e. CC ) $=
( cc wcel caddc co addcl syl2anc ) ABFGCFGBCHIFGDEBCJK $.
$}
Instead of many disjoint variable conditions:
${
$d x y $. $d x z $. $d F x $. $d ph x $. $d ph y $. $d F z $. $d F y $.
$d ph z $. $d y z $.
It is more readable to merge them:
${
$d F x y z $. $d ph x y z $.
There is a preference for more general theorems (i.e. easier to use) and fewer axioms.
Just try your best to make a label corresponding to ~ conventions-labels and more updated/relevantly the actual labels that exist. It is ok to fail on this as the reviewers will look at them.
- Size of pull requests: Try to make each PR readable - not so huge that it's very hard to review. Dividing one change into many might be needed.
- CI checks: See CONTRIBUTING.md. Basically, the metamath.exe
rewrapandsave proof */compressedcommands. You are encouraged tominimizeyour theorems. Also covers if thediscouragedfile needs regenerating. It's perfectly fine to let the CI fail and fix things after instead of before. -
changes-set.txt: This file covers 1. moves from mathbox to main and 2. main theorem statement or label changes (not proof), so update that if needed.
- ~ conventions
- ~ conventions-labels
- ~ conventions-comments
- https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md
This might be useful: