"Metamath is not considered to be a serious contender for large scale mathematical formalization work."

[Junyan Xu]

from page 2 of https://arxiv.org/pdf/1904.03241.pdf

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) 

Holophrasm is also mentioned.

The environment was presented on the AITP 2019 conference (held during last week): http://aitp-conference.org/2019/

[Mario Carneiro]

This is of course a step up from not being mentioned at all in surveys of extant theorem prover ecosystems. It's a related works section, I'm pretty sure researchers are contractually obligated to denigrate all opposition there. I'll just congratulate Daniel Whalen on getting another citation.

--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Jon P]

One question I would have about the future of formal systems is doesn't the problem decompose kind of into two parts? 

Part 1 is efficiently storing the proven theorems and providing ways for them to be easily checked. I think Metamath does this pretty well.

Part 2 is tools to assist in the process of generating new formal proofs. Surely these are relatively independent from part 1? Metamath has mmj2, the original exe and milpgame and probably more, which all have nice strengths. Presumably if Metamath had a really superb tool for this process (with things like this deep learning approach to automatically filling in missing sections) then it would be as good as anything?

I can't really compare MM with other theorem provers so I don't how it compares. Maybe there are a bunch of tradeoffs that are being made between speed and user friendliness and things like that? It just seems to me to be odd to say one language is better than another when a lot of what defines the difference is the tools.

[Giovanni Mascellani]

Hi,

Il 19/04/19 22:43, Jon P ha scritto:

> One question I would have about the future of formal systems is doesn't
> the problem decompose kind of into two parts? 

Yes, and I think that's where Metamath is particularly good: it clearly
decomposes the problem between (a) a format to describe proof, which in
itself is independent of any specific implementation of platform; (b) a
program to check the correctness of the proofs (actually many, in the
case of Metamath); and (c) the tooling to create and edit proofs. I am
not aware of many other systems that have the same clean architecture
(admittedly, I did not perform extensive research; but certainly the HOL
family is a big lump of everything together, and the concept of
exporting a proof in a program-independent format is very weak).

That might also be the reason while people expert in other systems might
fail to recognize the good architecture that there is underlying Metamath.

> Part 1 is efficiently storing the proven theorems and providing ways for
> them to be easily checked. I think Metamath does this pretty well.

Absolutely. HOL Light takes minutes just to get started (i.e., giving
you a prompt, not doing original work), to the extent that the official
suggestion is to use some obscure process checkpointing hack.

> Part 2 is tools to assist in the process of generating new formal
> proofs. Surely these are relatively independent from part 1? Metamath
> has mmj2, the original exe and milpgame and probably more, which all
> have nice strengths. Presumably if Metamath had a really superb tool for
> this process (with things like this deep learning approach to
> automatically filling in missing sections) then it would be as good as
> anything?

Right again. Metamath is currently lacking tooling to easily generate
proofs. This is something where HOL Light, on the contrary, is pretty
strong, and we should definitely try to adapt their ideas and solutions
to the Metamath workflow.

There still would be philosophical differences between Metamath and HOL,
on which the judgement might be in either direction depending on tastes
and objectives. But I don't think that Metamath would be inferior to
anything else in terms of large scale mathematical formalization. The
"Formalizing 100 theorems" challenge[1] already proves that Metamath is
doing pretty well, although to me most of the theorems in the challenge,
while definitely interesting and valuable, are a little too elementary
to really qualify as "large scale mathematics". E.g., I am a lot more
concerned of the lack of topological/differential manifolds than by the
lack of Buffon's needle problem.

[1] http://www.cs.ru.nl/~freek/100/

BTW, I take no merit for me about all of this, since for the moment I
haven't contributed nearly anything concretely helpful the Metamath.
Thanks to those who actually did the hard work!

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[OlivierBinda]

I say.

The design of MetaMath is pretty strong and has withstood the test of time.
Let's just build the tooling that will really make it shine and prove
them wrong.

I have been experimenting with metamath tooling and it already looks to
me like there is a lot that can be done there.
In one month, I hope to go even further (just started working on stuff
with antecedents, right now).
Time will tell...

Olivier

[Mario Carneiro]

No, metamath doesn't even have the Fibonacci numbers AFAIK. In fact, the formula would probably be used as the definition of the fibonacci numbers, because a Fibonacci style recursion would be more complicated to define. Then the trick would be showing that Fn is an integer, and the defining equations hold.

On Sun, Apr 21, 2019 at 9:35 AM j4n bur53 <burs...@gmail.com> wrote:

Was Binets Formula already
proved in meta math?

Just currious, a quick search didn't
show for example an Isabelle/HOL proof.

[Sauer, Andrew Jacob]

Metamath has strong induction, at indstr. It appears people haven't made much use of it though, is there a specific reason why?

On Sun, Apr 21, 2019 at 7:20 AM j4n bur53 <burs...@gmail.com> wrote:

I remember Isabelle/HOL has strong induction. You could
invoke it somehow, this was part of some exercise in 2015.

Deriving strong induction in meta math should be possible,
so I guess it would be even bootstrappable. But still its

a challenging mixed problem...

On Sunday, April 21, 2019 at 4:11:15 PM UTC+2, Mario Carneiro wrote:

No, metamath doesn't even have the Fibonacci numbers AFAIK. In fact, the formula would probably be used as the definition of the fibonacci numbers, because a Fibonacci style recursion would be more complicated to define. Then the trick would be showing that Fn is an integer, and the defining equations hold.

On Sun, Apr 21, 2019 at 9:35 AM j4n bur53 <burs...@gmail.com> wrote:

Was Binets Formula already
proved in meta math?

Just currious, a quick search didn't
show for example an Isabelle/HOL proof.

On Sunday, April 21, 2019 at 10:47:30 AM UTC+2, OlivierBinda wrote:

I say.

The design of MetaMath is pretty strong and has withstood the test of time.
Let's just build the tooling that will really make it shine and prove
them wrong.

I have been experimenting with metamath tooling and it already looks to
me like there is a lot that can be done there.
In one month, I hope to go even further (just started working on stuff
with antecedents, right now).
Time will tell...

Olivier

--
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 meta...@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Mario Carneiro]

I didn't say it couldn't be done, it's just not as easy as the alternative. In this case it's not strong induction we want but strong recursion; you can do this with recs but there is a lot of translation to do. Using seq on a pair would be the easiest approach. The Bernoulli numbers are defined by a strong recursion using wrecs. Having an explicit formula to write down is much simpler in metamath.

[Jens-Wolfhard Schicke-Uffmann]

https://github.com/Drahflow/Igor
currently gets support for interactive reasoning over goals made of a
set of antecedents and a statement. The final metamath formalization
is then automatically compiled from that. I hope to complete the
formal verification of my non-trivial (but nearly so) Raspberry Firmware this
year.

The earlier approach in which the display of antecedents was automated,
but underneath it was all materialized |- ( ph -> ps ) statements all the time
did not scale well, because much memory was wasted representing all the
intermediate resorting steps of the parts of the ph.


Check my (much) earlier mail for some details:
https://groups.google.com/forum/#!msg/metamath/113Y5z1a_PQ/uY_eubjqAgAJ
(Project was suspended for a long time while I did completely unrelated
stuff.)


All the best,
Drahflow

[Thierry Arnoux]

FYI, set.mm now has a “strong recursion sequence” operator ‘ seqstr ‘, and the Fibonacci sequence as an example:

http://us2.metamath.org:88/mpeuni/df-fib.html
BR,

_

Thierry

[Benoit]

You could define the Catalan numbers via the usual recursion relation and then try to prove the closed form. This would be an achievement.

On Sunday, April 28, 2019 at 5:10:50 PM UTC+2, j4n bur53 wrote:

prove forall n Q(n), instead forall n P(n). I guess forall n Q(n),
implies forall n P(n). So fibonacci is kind of a limited horizon
recursion, we only need to look back to a fixed number k of
elements where k=2, which makes it not a truely strong

recursion example, where k would be unbounded. Somehow I
am at loss, what a true example could be, although I have seen
some on the internet, but they were more complex, where the
objects what needs to look back were polynomials. So a

more number theoretic example, I did not yet find.

Am Sonntag, 28. April 2019 17:04:36 UTC+2 schrieb j4n bur53:

Cool!

BTW: The discussion elsewhere about strong vs weak, took an interesting
turn. We are still looking for a convincing example for strong induction. Since
somebody suggested to solve Binets Formula problem, with a different

induction predicate

    So instead prove via strong induction:
            P(n) <=>  fib(n) = binets_formula(n)

One can try the following weak induction:

    Simply prove via weak induction:
            Q(n) <=> P(n) /\ P(n+1)

    Right?

But this wont say strong induction is useless. It says only that our
pedagogical search for a better illustration of strong induction cases
has not yet succeeded.

To unsubscribe from this group and stop receiving emails from it, send an email to meta...@googlegroups.com.

[Norman Megill]

On Friday, May 10, 2019 at 8:17:01 PM UTC-4, j4n bur53 wrote:

Thanks for the hint! Catalan numbers could indeed
be an interesting candidate. Now discussion started
meandering around axiom of choice, and I got

lost in metamath.

   So to see
   Theorem ac5 => Theorem ac7

   I would need to look at:
   http://us.metamath.org/mpegif/dfac4.html

 

What I want to see would be some byproduct?

I'm not sure what you mean by byproduct.
 

Why is dfac4 called dfxxx like a definition?

It is a logically equivalent variant of actual definition df-ac.  It may be more convenient for some proofs than df-ac.  dfxxx is a naming convention we sometimes use for logically equivalent variants of definitions, but otherwise it is just a theorem like any other.  The name itself has no intrinsic meaning; we could have called it acequiv4 or something.

Because it can be used like a definition?

In a sense yes, but again it's just another theorem.  If we wanted we could have used it in place of the current definition df-ac (then we would derive what is now df-ac as a theorem).  As far as using it in a proof, there is no intrinsic difference whether a referenced statement is a definition ($a) or a theorem ($p).
 
Norm

[Norman Megill]

On Saturday, May 11, 2019 at 8:28:28 AM UTC-4, j4n bur53 wrote:

Byproduct as in, simplified view:

       A <=> B
       --------------------------
       (A => B) & (B => A)
      ----------------------------
       A => B

This is theorem biimpi.
http://us.metamath.org/mpeuni/biimpi.html
 

So A=>B is a spinoff of having a proof A<=>B. But proofs work
more complex showing (CHOICE <=> A) <=> (CHOICE <=> B).

We don't do that in any proof that I'm aware of.  But if we needed it for some reason and the two sides are dfac2 and dfac4, then you can apply 2th to achieve the above.
http://us.metamath.org/mpeuni/2th.html
http://us.metamath.org/mpeuni/dfac2.html
http://us.metamath.org/mpeuni/dfac4.html

If your goal is to eliminate CHOICE and achieve A <=> B, you don't need this.  it can be done in one step by applying bitr3i to dfac2 and dfac4.
http://us.metamath.org/mpeuni/bitr3i.html

Or interim |- CHOICE is derived as here:

    http://us.metamath.org/mpegif/axac2.html

The CHOICE in intermediate step 3 of that proof is derived from ax-ac.  You can see ax-ac in the "This theorem was proved from axioms" list on that web page.

The standalone CHOICE in theorem axac3 is derived from ax-ac2.  You can see ax-ac2 in "This theorem was proved from axioms" on web page
http://us.metamath.org/mpeuni/axac3.html

Axiom ax-ac was chosen many years ago as the "official" AC because of its brevity.  Axiom ax-ac2 was added later because it is equivalent to the version usually used in the literature.

Axioms ax-ac and ax-ac2 are not equivalent under ZF minus Regularity.  ax-ac implies ax-ac2 under ZF minus Regularity.  However, ax-ac2 does not imply ax-ac unless we use Regularity.
http://us.metamath.org/mpeuni/ax-ac.html
http://us.metamath.org/mpeuni/ax-ac2.html

We chose the symbol CHOICE to represent ax-ac2.
http://us.metamath.org/mpeuni/df-ac.html
The purpose of theorem axac2 is to show that ax-ac inplies ax-ac2 under ZF minus Regularity (note that ax-reg is not included in "This theorem was proved from axioms" on the web page http://us.metamath.org/mpeuni/axac2.html).
 

There are also "byproduct" helpers around, not of the "=>" kind,
more of the "<=>". But this helper explicitly mentions CHOICE,
like this here:

     http://us.metamath.org/mpegif/axaci.html

Yes, this is a "helper" theorem used to shorten some later proofs.

Is this "architecture" genuinly metamath, or was it borrowed
from somewhere else?

I'm don't know what you mean by "architecture".  Most of what I mentioned above are just applications of standard propositional calculus.  I don't think there is any logic used that is unique to Metamath.

Norm

[Mario Carneiro]

Hi Jan,

Do you think you could ask your questions on a new thread? When you respond with unrelated comments on a thread it makes it more difficult to follow.

On Fri, May 17, 2019 at 11:47 AM j4n bur53 <burs...@gmail.com> wrote:

Disclaimer: I call here A x B "sum" type and A -> B "product"
type. Not to be confused with disjoint sum A + B which is
not the same as cross product A x B.

Am Freitag, 17. Mai 2019 17:31:16 UTC+2 schrieb j4n bur53:

Now there was an interesting thread somewhere else.
We observed that when we type predicates as:

     Unary predicate:   D

     Binary predicate:  D x D

We might obtain, i.e. shape shifting between arities, not
allowed in first order logic, FOL:

     P(<x,y>) <=> P(x,y)

If P is a class symbol, does the same also happen in
metamath somehow?  My own solution to the problem would
be to see unary respectively binary predicates as has
having this signature:

     Unary predicate:   D -> B

     Binary predicate:  D -> D -> B

where B={0,1}. But not sure how to resurect class
symbols then, and create a metamath zero, well I guess
it would be a metamath two, since metamath zero is
already used for an other project, a metamath with arity.

But there are a lot of options around. What should
the pairing function do? Should we have sum types at
all. The initial example assumes pairing function is, i.e.
without sum type, <_,_> : D -> D -> D.

but if we have sum type, we could say pair is <_,_> :
D -> D -> D x D. but in set theory there might be an inclusion
of the sum type, i.e. D x D subset D. So that sum types
dont seem to be viable to fix anything.

Am Sonntag, 12. Mai 2019 20:03:12 UTC+2 schrieb j4n bur53:

Catalan numbers are natural numbers. A new question.
Was there ever already done something in metamath

about Cantor Pairing? Some theorems in metamath
about this little quadratic polynomial:

     Cantor polynomial
   P(x,y) = 1/2 ((x+y)*(x+y+1)) + x

P ( x , y ) := 1 2 ( ( x + y ) 2 + 3 x + y ) {\displaystyle P(x,y):={\frac {1}{2}}((x+y)^{2}+3x+y)}     

    https://en.wikipedia.org/wiki/Fueter%E2%80%93P%C3%B3lya_theorem

Googling "pairing" site:metamath.org
didn't give me something. Just currious.

Am Samstag, 11. Mai 2019 02:17:01 UTC+2 schrieb j4n bur53:

Thanks for the hint! Catalan numbers could indeed
be an interesting candidate. Now discussion started
meandering around axiom of choice, and I got

lost in metamath.

   So to see
   Theorem ac5 => Theorem ac7

   I would need to look at:
   http://us.metamath.org/mpegif/dfac4.html

What I want to see would be some byproduct?

Why is dfac4 called dfxxx like a definition?

Because it can be used like a definition?

To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8b306044-0d76-4f24-9bc4-aec9423b3a90%40googlegroups.com.

[Mario Carneiro]

Then make a single thread for all your embryonic thoughts. Please don't pollute everyone else's threads with unrelated stuff.

On Fri, May 17, 2019 at 12:53 PM j4n bur53 <burs...@gmail.com> wrote:

Because I have every once a day an idea, I didn't wanted to
contributed to the explosion of threads by just posting every

new embrionic thought, in a new thread.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/8b306044-0d76-4f24-9bc4-aec9423b3a90%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4fb5bb2e-1705-45d8-8d29-20b24bfad44f%40googlegroups.com.

[Mario Carneiro]

Hi Jan,

I'm responding to the sustained pattern of behavior as a moderator on this mailing list. This is not meant to be an insult, it is a request to conform to etiquette. Over half the posts in this thread are from you, responding to yourself. If you want to share your thoughts do it on a thread labeled "Jan's thoughts" or labeled with your question. Having a number of short threads is not a horrible thing, but responding with off topic things defeats the whole point of threads. If you can't stay on topic I will have to start deleting posts and ask you to repost in an appropriate manner.

In response to your last question about unary vs binary predicates: We use A -> B to denote a function with domain A, and A x B -> C to denote a function with domain A x B, usually thought of as a binary function. There is no question of distinguishing them here; it is presumed that the domain is known and fixed. If you want to tell the difference between different arities, you can use Word A -> B, where Word A is the collection of all strings with elements in A. This is the disjoint union of A^n for all n < omega. You can also use A ^ (0 ..^ n) -> B where n is a natural number to say that the function is specifically n-ary. These sets are distinguishable, i.e. A ^ (0..^1) and A ^ (0..^2) are disjoint.

It's not clear to me what you are attempting to achieve. If you want tuples, we have tuples. They can have their lengths built in or not. There is a variety of notation for them.

Have you tried proving something in metamath? If you start using metamath you will find the answer to most of your questions.

DO NOT RESPOND ON THIS THREAD. Make a new one if you want to respond to me or yourself.

Mario

On Fri, May 17, 2019 at 2:15 PM j4n bur53 <burs...@gmail.com> wrote:

You also answered in the past here:

Mario Carneiro
https://groups.google.com/d/msg/metamath/La4LEDM5ASI/OM8yhrU4CQAJ

Whats so different in my new question? Did I provoke something
because I mentioned metamath zero? I don't know how metamath
zero would handle the case. I only wanted to find a name

for what I am working on. So I called it metamath one. But
if you feel better, I can also call it metamath minus one. If
this makes you feel better, well then.

Ha Ha, some people are really fun, and they will never apologize.

Am Freitag, 17. Mai 2019 20:06:24 UTC+2 schrieb j4n bur53:

Also Norman Megill didn't mind answering a question here.
I guess he has better manners than you have. Insulting people
with no grounds.

Am Freitag, 17. Mai 2019 20:05:08 UTC+2 schrieb j4n bur53:

So far I have only use this thread for most of my thoughts. You can't
say I have polluted everyones elses thread, this a false allegation

and some harassement.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4fb5bb2e-1705-45d8-8d29-20b24bfad44f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2ea5d8cf-1dd1-45fe-aaa7-1c7db17e2799%40googlegroups.com.

[vvs]

Probably people from different projects have way too different goals in mind. I'd say that Metamath is more oriented towards math foundations while other projects have tools and applications for verification of models in electronics etc. How hard it could be to automatically generate some high level programming language code in metamath to describe such models and verify or simulate them? Indeed, it might be ignored by those who seek industrial applications.

[Giovanni Mascellani]

Hi,

Il 19/05/19 00:07, vvs ha scritto:

I tend to think Metamath as oriented towards (so-called) "pure"
mathematics in general, not specifically mathematical foundations
(although, of course, foundations is where you begin, and definitely
there are people around mostly focussing on foundations). My personal
long-term hope is that one day it will be natural for maths researchers
to attach formal proofs of their results to their papers, so that
everybody can check them and understand what sometimes is missing in the
informal proof.

Indeed, I believe that Metamath might not be the best choice for
verification of "real-life" applications, like from electronics or
software engineering, because it tends to be very explicit (for example,
storing proofs as sequences of steps, and not as programs that generate
those steps; and being geared towards actually visualizing the proofs,
not just checking them, like in the beautiful web pages generated by the
Metamath Proof Explorer). This is good when you want to understand maths
proofs, but it is a bit less so when you have to deal with very
technical proofs that define very complicated systems that you still
have to describe with a linear formula.

However, the word "Metamath" can means at least three different things:
the underlying abstract data model (i.e., basically the concept of
substitution with distinct variables), the file format used today and
the Metamath reference implementation written by Norman used today. Of
these, in my opinion, only the first one is the really persistent one.
The other two can change, and if the first one remains it is easy to
convert from one to another and still remain compatible. With that in
mind, the possibilities are many more.

As a matter of facts, Mario is already experimenting with x86 semantics
in his MM0 repository, although at this point I do not really know what
is the status and the plan. He wrote something in this post:

https://groups.google.com/d/msg/metamath/A2p5GPDwXxw/OUo8ZKGIAgAJ

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[vvs]

On Sunday, May 19, 2019 at 10:07:38 AM UTC+3, Giovanni Mascellani wrote:

As a matter of facts, Mario is already experimenting with x86 semantics
in his MM0 repository, although at this point I do not really know what
is the status and the plan. He wrote something in this post:

Yes, when somebody talking about "large scale" formalization they probably mean just some form of automation of proofs. Working with semantic tools should at least make such claims harder to defend. I think that the best choice would be to study and even implement support for already established frameworks, e.g. http://www.cl.cam.ac.uk/~pes20/sail/ I doubt they will be impressed by just pure mathematics.

[Mario Carneiro]

My x86 formalization is actually based on the Sail x86 formalization. I thought about translating it automatically, but I don't have an easy way to access the internal data structures or otherwise parse what appears to be a quite complicated (aka "friendly") language.

--

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/8880c819-6bd9-4fb8-bae5-afe317e8157e%40googlegroups.com.

[Junyan Xu]

In the context of the paper they are probably referring to the proof of the Kepler conjecture (in HOL Light), a major part of the dataset they use for benchmarking.