This is nice work Stanislas, thank you. On Friday, July 3, 2020 at 5:09:55 AM UTC-4, Stanislas Polu wrote:
- `1re` uses more axioms but is much simpler (how do we feel about > that given the comment there?). > A problem with this particular proof is that it uses df-1, which has the tag "(New usage is discouraged.)". Let me explain a little about how the complex numbers are introduced. Our overall goal in set.mm is to show mathematics that follows from the ZFC axioms. For complex numbers, we construct a model (a set of axioms stated as $p statements) starting from ZFC axioms. We then restate these derived axioms ($p statements) as actual axioms ($a statements) in order to (1) make the complex number development independent from the construction (so that alternate models could in principle be "plugged in") and (2) make it easier to see what complex number axioms are needed for a particular complex number theorem. So, for example, we derive ax1cn in the model part, then restate that theorem as axiom ax-1cn. (To help ensure we're not cheating by introducing new axioms beyond ZFC, the 'verify markup' command in metamath.exe checks that each ax-* $a statement exactly matches an earlier $p statement with the "-" removed, if such a $p statement exists.) To help prevent the accidental usage of the complex number construction when we later use complex numbers, we have "(New usage is discouraged.)" in every statement in the development of the complex number model. df-1 is one such statement, since it might change if we used a different complex number construction. For our metamath.exe and mmj2 proof assistants, the string "(New usage is discouraged.)" in a comment tells the proof assistant not to consider that statement for use in a proof being developed. In addition, the Travis run that is done after each pull request checks that the usage of statements with "(New usage is discouraged.)" didn't change as a result of the PR (unless it was done intentionally and the user has supplied a regenerated "discouraged" file as part of the PR). I would recommend that the OpenAI assistant check statement descriptions for the string "(New usage is discouraged.)" and avoid considering them for use in proofs. (The metamath.exe command 'write source set.mm /rewrap' currently prevents this string from being broken across lines, but I'm not sure we want to guarantee that, nor can we guarantee the '/rewrap' command was run. But for a quick and dirty check you can assume it's not broken across lines and refine it later with a TODO.) Norm -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dd8ea31b-8799-4591-a6d4-688c519eedado%40googlegroups.com.
