update conventions#"Acceptable shorter proofs"

[icecream17]

Current content (additional emphasis added):

• Acceptable shorter proofs. Shorter proofs are welcome, and any shorter proof we accept will be acknowledged in the theorem description. However, in some cases a proof may be "shorter" or not depending on how it is formatted. This section provides general guidelines.

  Usually we automatically accept shorter proofs that (1) shorten the set.mm file (with compressed proofs), (2) reduce the size of the HTML file generated with SHOW STATEMENT xx / HTML, (3) use only existing, unmodified theorems in the database (the order of theorems may be changed, though), and (4) use no additional axioms. Usually we will also automatically accept a new theorem that is used to shorten multiple proofs, if the total size of set.mm (including the comment of the new theorem, not including the acknowledgment) decreases as a result.

  In borderline cases, we typically place more importance on the number of compressed proof steps and less on the length of the label section (since the names are in principle arbitrary). If two proofs have the same number of compressed proof steps, we will typically give preference to the one with the smaller number of different labels, or if these numbers are the same, the proof with the fewest number of characters that the proofs happen to have by chance when label lengths are included.

  A few theorems have a longer proof than necessary in order to avoid the use of certain axioms, for pedagogical purposes, and for other reasons. These theorems will (or should) have a "(Proof modification is discouraged.)" tag in their description. For example, idALT 23 shows a proof directly from axioms. Shorter proofs for such cases won't be accepted, of course, unless the criteria described continues to be satisfied.

Updates todo:

1. In the third paragraph, I think the first sentence was used to declare that Use bicom1 and syl in bicomd #2601 was not a valid shortening. However, today (2025-07-01), I just noticed the last sentence, which would seem to imply that it is. Either the conventions needed updating on this point, or the shortening is valid. (Probably the former?)
2. The fourth paragraph should probably mention $j axiom tags:

   In the case of avoiding axioms, a $j usage comment should be used just after the proof, for example $( $j usage '19.21v' avoids 'ax-6' 'ax-7' 'ax-12'; $).

[digama0]

In the third paragraph, I think the first sentence was used to declare that #2601 was not a valid shortening. However, today (2025-07-01), I just noticed the last sentence, which would seem to imply that it is. Either the conventions needed updating on this point, or the shortening is valid. (Probably the former?)

I don't see the contradiction. The last sentence of the third paragraph seems pretty clear that it is to be used as a tiebreaker, so the first sentence takes precedence.

[icecream17]

The contradiction is between the conventions and the rejection of #2601 - it would have been accepted, strictly speaking.

[jkingdon]

2. The fourth paragraph should probably mention $j axiom tags

Good thinking. In that case I don't think the "Proof modification is discouraged" would be needed.