On Tue, Apr 2, 2024 at 6:56 PM Anarcocap-socdem <
jordi.molins.coron...@gmail.com> wrote:
> Thank you very much for the answer.
>
> Let us see if I understand this:
>
> Let us assume I take the 619 different subtheorems used in 2p2e4 (I get
> this number, 619, by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS). These 619
> subtheorems can be listed by doing show trace_back 2p2e4. The total number
> of steps of these 619 subtheorems is 12178 (again, this number is obtained
> by doing SHOW TRACE_BACK 2p2e4 /COUNT_STEPS).
>
> So, is it correct to say the following:
>
> - I can create a new file, let us call it set_simplified.mm, which
> corresponds to taking set.mm, and only keeping the 619 subtheorems used
> in the proof of 2p2e4.
> - I can run python3 mmverify.py set_simplified.mm --logfile set.log to
> check that the proof is correct. mmverify.py has about 690 lines.
>
> So, with 12178 steps, plus 690 lines, I can get a full proof of 2p2e4. All
> these steps could be written in a pdf file (long, but not unreasonably
> long).
>
> Is this correct? Or maybe the way I have defined set_simplified.mm is
> "too simplified"?
>
Yes, that is basically correct. Strictly speaking though it is "too
simplified", because it doesn't account for statement types other than $p /
$a :
* ${ , $} - obviously we need these for grouping a statement with its
hypotheses
* $e - (hypotheses) these are "attached" to each theorem and usually
directly precede them, although sometimes they can be in the same scope as
an earlier theorem and shared across multiple theorems
* $d - (disjoint variable conditions) these are also hypothesis-like in
their scoping pattern and semantics
* $v, $f - (variable declarations) for set.mm these are basically global,
but there is still a well defined notion of "use" of a variable: just look
for its token in any of the 619 subtheorems. If you see it then it must be
declared, otherwise it can be dropped.
* $c - (constant declarations) These are global, and have the same kind of
"use" as variables: if you see it in the $p ... $= or $a ... $. text then
it must be declared first.
For all these reasons, you probably want to use a "metamath aware" slicer
for constructing these *_simplified.mm databases. But this is all very
straightforward and will not add much on top of the 619 theorems you
identified. None of these count as "steps" though toward the 12178 step
count; these are for proof steps (I don't know whether syntax steps are
included or omitted in the count), and the best you can say about its
relation to the simplified.mm file is that every step requires at least one
character so set_simplified.mm should be at least 12178 characters and
probably more because of theorem statements, delimiters, formatting, and
comments if you are keeping them.
In general, no this process will not produce long proofs. In fact it's
about as short as we know how to make them, since this is taking full
advantage of metamath's abstraction and reuse mechanisms, and the library
itself is optimized for overall proof size. However you can find some
inefficiencies in this process because set.mm is trying to prove more than
just 2+2 = 4 so it will prove things in "unnecessary" generality that
becomes pure overhead once you cut literally everything else out. So it's
likely that after extracting such a database you can run minimizers over
the code and get still more savings.
> On Monday, April 1, 2024 at 10:48:46 PM UTC+2 di....@gmail.com wrote:
>
>> > 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated
>> that "A longest path back to an axiom from 2 + 2 = 4 is *184 layers* deep".
>> However, if I run show trace_back 2p2e4 /count_steps, it is stated that
>> "The maximum path length is 84". Is there a typo somewhere? (84 != 184).
>>
>> Note that that statistic is one of those that will go out of date quickly
>> due to changes in the library structure. So you should not expect it to be
>> exact, unless we have an automated mechanism for keeping it up to date, and
>> we don't currently. However, there is one major change between when that
>> text was written and now which significantly decreased most of the numbers
>> quoted, which is the isolation of the real numbers from their construction.
>> 2+2 = 4 is a theorem very close to the axioms of real numbers, so it was
>> reduced from something depending on the entire stack of set theory and the
>> construction, down to just a few direct axiom applications (plus still a
>> bunch of set theory because of the use of df-ov "operation value" for
>> expressing the + function, defined in the set theory section).
>>
>> In order to get something closer to the "true" original numbers, you
>> should replace "ax-mulcom $a ... $." with ax-mulcom $p ... $= <apply
>> axmulcom> $. and similarly for all the other axioms in the same section.
>> This will allow metamath-exe to see that uses of these axioms actually
>> depend on a big stack of other lemmas when calculating statistics like max
>> depth and full-expansion theorem counts.
>>
>> > 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a
>> total of 619 different subtheorems are used. The statement and subtheorems
>> have a total of 12178 actual steps (...) The proof would have 5887862241803
>> =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is
>> the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess
>> that 12178 steps refers to the case in which we take the axioms of the
>> complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms
>> of the complex numbers, starting from ZFC. But I am not 100% sure, and I
>> would like to have confirmation of that.
>>
>> No, this is not about that. Metamath theorems are able to refer to
>> previous theorems multiple times, in multiple concrete instantiations. That
>> is, a theorem is really a "theorem schema" over the assignments to the wff
>> and class variables. If you wanted to perform the same proof in pure first
>> order logic, you would have to redo the proof for every choice of those wff
>> variables. So the statistic here (also calculated by metamath-exe) is
>> working out an approximation to the (exponential) speedup this
>> accomplishes, by seeing how many steps would have been taken if you had to
>> replay each use of each theorem. Effectively, you can think of this as
>> treating every metamath theorem as a macro which expands to a proof
>> containing more macro references, and if we macro-expand everything all
>> that remains are direct references to the axioms. It's easy to get
>> exponential growth in this process, since theorem 2 can use theorem 1
>> twice, theorem 3 uses theorem 2 twice and so on. Of course the metamath
>> library is not quite so pathological as that, but the nature of the process
>> is still exponential, where the base is related to the density of
>> converging paths in the DAG of theorem references.
>>
>> > 3. Is there some way to print/export to file the 12178 steps, and even
>> the 5.9 x 10^12 steps, all at once? I ask this since running show
>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the
>> subtheorems, not the steps themselves. And I have been unable to find a
>> command that gives the full number of steps, all at the same time.
>>
>> As far as I know, no. Both of these numbers are calculated by the
>> metamath-exe tool, using the command "SHOW TRACE_BACK 2p2e4 /COUNT_STEPS".
>> Internally, it only creates and manipulates the numbers, it doesn't
>> actually perform the expansion (which would take exponentially long just to
>> output). For the former number (12178 steps), an approximation to this is
>> to just "show proof *" which will print all proofs, or look at the entire
>> metamath web site on disk, which contains every step of every theorem. The
>> 12178 steps are a subset of those, and you can get metamath-exe to print
>> out all of the relevant theorems using "show trace_back 2p2e4" alone.
>>
>> That said, it is certainly possible to calculate the actual 5.9 x 10^12
>> steps if you are interested in such a programming project. But be aware
>> that the steps can also get pretty large in the process (I think also
>> exponential in general). Although I'm sure your terabyte drive has better
>> things to do...
>>
>> Mario Carneiro
>>
>> On Mon, Apr 1, 2024 at 9:44 AM Anarcocap-socdem <jordi.moli...@gmail.com>
>> wrote:
>>
>>> Hello, I am trying to understand 2p2e4, as an excuse to understand
>>> metamath better.
>>>
>>> I have a few questions:
>>>
>>> 1. In https://us.metamath.org/mpeuni/mmset.html#trivia, it is stated
>>> that "A longest path back to an axiom from 2 + 2 = 4 is *184 layers*
>>> deep". However, if I run show trace_back 2p2e4 /count_steps, it is
>>> stated that "The maximum path length is 84". Is there a typo somewhere? (84
>>> != 184).
>>> 2. If I run show trace_back 2p2e4 /count_steps, it is stated that " a
>>> total of 619 different subtheorems are used. The statement and subtheorems
>>> have a total of 12178 actual steps (...) The proof would have 5887862241803
>>> =~ 5.9 x 10^12 steps if fully expanded back to axiom references.". What is
>>> the difference between the 12178 steps, and the 5.9 x 10^12 steps? I guess
>>> that 12178 steps refers to the case in which we take the axioms of the
>>> complex numbers as "axioms", and 5.9 x 10^12 when we also prove the axioms
>>> of the complex numbers, starting from ZFC. But I am not 100% sure, and I
>>> would like to have confirmation of that.
>>> 3. Is there some way to print/export to file the 12178 steps, and even
>>> the 5.9 x 10^12 steps, all at once? I ask this since running show
>>> trace_back 2p2e4 /tree gives me a tree, but with only the name of the
>>> subtheorems, not the steps themselves. And I have been unable to find a
>>> command that gives the full number of steps, all at the same time.
>>>
>>> Thank you for your work on this great project.
>>>
>>> --
>>> 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+u...@googlegroups.com.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/metamath/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com
>>> <https://groups.google.com/d/msgid/metamath/f3cb2f43-8608-4293-b2da-af283d9676fen%40googlegroups.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>> --
> 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/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/68e0c4f9-d0c4-4261-a949-610bdbd772ebn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAFXXJSuEfYJHHKvvs%3DaOX7Rc916dAVhtpEF6D7aAzXHuFv_xkw%40mail.gmail.com.
