695 views

Skip to first unread message

Mar 26, 2020, 12:24:02 PM3/26/20

to meta...@googlegroups.com

Hi!

At OpenAI we've been exploring the use of deep learning for formal

math for the past couple months. We've worked a lot with Metamath

whose simplicity makes it very amenable to deep learning.

Today, I submitted a PR containing a sample of proofs that were found

by our models and that are substantially shorter than their human

curated counterparts:

https://github.com/metamath/set.mm/pull/1547

We're very curious to hear from the community on whether this is

useful. Additionally, if the authors of the original proofs shortened

by this PR have qualitative feedback on the proposed versions, we'd be

keen on hearing from them as well, obviously.

As mentioned in the PR the models were run on a sample of ~1k proofs

from set.mm so we could probably get 45 times as many shorter proofs

if there is interest for it!

Looking forward to your feedback and comments.

-stan

At OpenAI we've been exploring the use of deep learning for formal

math for the past couple months. We've worked a lot with Metamath

whose simplicity makes it very amenable to deep learning.

Today, I submitted a PR containing a sample of proofs that were found

by our models and that are substantially shorter than their human

curated counterparts:

https://github.com/metamath/set.mm/pull/1547

We're very curious to hear from the community on whether this is

useful. Additionally, if the authors of the original proofs shortened

by this PR have qualitative feedback on the proposed versions, we'd be

keen on hearing from them as well, obviously.

As mentioned in the PR the models were run on a sample of ~1k proofs

from set.mm so we could probably get 45 times as many shorter proofs

if there is interest for it!

Looking forward to your feedback and comments.

-stan

Mar 26, 2020, 12:54:25 PM3/26/20

to Metamath

That's very interesting and promising !

Did you make sure that no new axiom dependencies were introduced in the proofs ? Is it possible to keep the older proofs as "xxxOLD" with the comment "Old proof of ~ xxx . Obsolete as of 26-Mar-2020. " and both discouragement tags ? This would ease comparisons and might give some insight on the kind of shortening introduced.

Is it possible to have some details on the model that you used ?

Benoît

Mar 26, 2020, 1:01:42 PM3/26/20

to meta...@googlegroups.com

Thanks Benoit,

Great points. Is there a metamath-exe way to compute the axioms dependency so that I can run that analysis?

Concerning keeping an OLD version, happy to do so. I’ll update the PR accordingly unless I hear otherwise.

I’ll prepare a summary of our approach to share with the community as well.

Best,

-stan

--

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/833aa5a4-23f0-4a30-bbaf-b49acaa3a510%40googlegroups.com.

Mar 26, 2020, 1:03:41 PM3/26/20

to meta...@googlegroups.com

I'm really intersted by this. I'll look at it when I can (in some

months) as I am overwhelmed right now.

But this is definetely on my to look at list because this will be really

useful for my project.

Many thanks for the link.

Best regards,

Olivier

months) as I am overwhelmed right now.

But this is definetely on my to look at list because this will be really

useful for my project.

Many thanks for the link.

Best regards,

Olivier

Mar 26, 2020, 1:03:49 PM3/26/20

to meta...@googlegroups.com

Also concerning axioms dependency I presume there is a tension between proof length and axiom dependency size that is probably more prevalent for low level theorems and much less important for higher level theorems where proof length is probably the only thing that matters?

Is there any consensus on that?

-stan

Mar 26, 2020, 1:28:37 PM3/26/20

to 'Stanislas Polu' via Metamath

Interesting stuff. I've noticed some possible shortenings which also were caught by this tool or least are of the same sort. For example, negdii could use negdi but doesn't, perhaps because negdi didn't exist when negdii was first added. But having an automated way of finding them (beyond what the minimizer can do) can potentially make those shortenings more likely to happen.

I didn't look at this in great detail, but based on a first glance, it seems to be one of the more promising automated systems for metamath proofs (and it isn't the only one we have seen).

I didn't look at this in great detail, but based on a first glance, it seems to be one of the more promising automated systems for metamath proofs (and it isn't the only one we have seen).

Mar 26, 2020, 2:15:20 PM3/26/20

to meta...@googlegroups.com

Uhmm, well length^2 is difficult where 1 x 3V2 x 3V2 x 3V2 = 2 ; in the mid-section (3V2)^2. ( a Multi-plecation of the “length” where the cube doubles)

__ __

1+

__ __

0,25992104989487316476721060727823 (=3V2)

__ __

+

__ __

0,32748000207332630998449503199408

__ __

+

__ __

0,41259894803180052524829436072769

__ __

=2

__ __

Length ^2 = squared surface area. Hence Length ^2 = not another length. In fact it is.

__ __

Increasing and decreasing (shortening) are thesame like +1 or -1.

__ __

Maybe I don’t really get the point,

__ __

With friendly regards,

__ __

Dirk-Anton Broersen

__ __

Verzonden vanuit Mail voor Windows 10

To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CACZd_0yWZPj0_Eudmw6MU4AJWbiUTewtX0uCf4yJBxET2voajQ%40mail.gmail.com.

__ __

Mar 26, 2020, 2:31:02 PM3/26/20

to meta...@googlegroups.com

You can do

MM>show trace_back xxx /axioms

or

MM>show trace_back xxx /match ax-*

for details, see

MM>help show trace_back

Indeed, there is a balance between axiom dependencies and proof length, but it seems to happen not so often. Typically, in those cases, one keeps both proofs with the label "xxxALT" for the shorter proof using more axioms.

Benoît

Mar 26, 2020, 4:10:13 PM3/26/20

to meta...@googlegroups.com

As an example for prime-number analysis I created a programm in C++

__ __

Maybe I can create such a file, but I see that a formula must be applied in order to get a mathematical outcome.

__ __

With friendly regards,

__ __

Dirk-Anton Broersen

__ __

__ __

Verzonden vanuit Mail voor Windows 10

__ __

**Van: **'Stanislas Polu' via Metamath

**Verzonden: **donderdag 26 maart 2020 18:01

**Aan: **meta...@googlegroups.com

**Onderwerp: **Re: [Metamath] Re: Deep Learning powered proof shortening

__ __

Thanks Benoit,

To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CACZd_0xGsge-GVOUnn06V%3DEKKmtZ25by%3DhCxRkjBZeZ1FWm__g%40mail.gmail.com.

__ __

Mar 27, 2020, 6:55:01 PM3/27/20

to Metamath

I just found an even shorter proof for ra4:

---------Clip out the proof below this line to put it in the source file:

( wi wral r19.21 biimpi ) ABFCDGABCDGFABCDEHI $.

---------The proof of "ra4" (45 bytes) ends above this line.

( wi wral r19.21 biimpi ) ABFCDGABCDGFABCDEHI $.

---------The proof of "ra4" (45 bytes) ends above this line.

whereas the one recently found by OpenAI is:

---------Clip out the proof below this line to put it in the source file:

( wnf wi wral r19.21t biimpd ax-mp ) ACFZABGCDHZABCDHGZGELMNABCDIJK $.

---------The proof of "ra4" (67 bytes) ends above this line.

( wnf wi wral r19.21t biimpd ax-mp ) ACFZABGCDHZABCDHGZGELMNABCDIJK $.

---------The proof of "ra4" (67 bytes) ends above this line.

I'm going to submit it in a new PR.

Benoît

Mar 27, 2020, 7:29:41 PM3/27/20

to Metamath

I hope you can run OpenAI on more proofs. Looking at some the first shortenings, it looks like it can behave as a more efficient "minimize_with" in some cases where there are many "weakenings". For instance, ~mideulem and ~midexlem use a lot of weakenings in the form of adantr, adantlr, ad2antrr, simplr, simprl... Could you run OpenAI on these two theorems to see what it does ?

Benoît

Mar 28, 2020, 3:34:05 AM3/28/20

to meta...@googlegroups.com

We plan to run it on a broader scale for sure.

I will check the two theorems as well today.

Thanks for your suggestions!

-stan

On Sat, Mar 28, 2020 at 12:29 AM Benoit <benoit...@gmail.com> wrote:

I hope you can run OpenAI on more proofs. Looking at some the first shortenings, it looks like it can behave as a more efficient "minimize_with" in some cases where there are many "weakenings". For instance, ~mideulem and ~midexlem use a lot of weakenings in the form of adantr, adantlr, ad2antrr, simplr, simprl... Could you run OpenAI on these two theorems to see what it does ?Benoît

--

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/b1bab644-ea9f-49ba-8238-0377228266ab%40googlegroups.com.

Mar 28, 2020, 10:53:05 AM3/28/20

to Metamath

Posted per FL's request. - Norm

-------- Forwarded Message --------

Subject: Stanislas' engine

Resent-From: nm

Date: Sat, 28 Mar 2020 14:53:18 +0100 (CET)

From: fl

To: Megill, Norman

Hi Norm,

Could you ask Stanislas how long

dors it take to minimize a proof

and would it be possible to launcher

minimize_with and Stanislas' engine

to compare the results. And I

guess the neural network must

be made again for each new version

of set.mm, so how long does it take

to train the network.

--

FL

-------- Forwarded Message --------

Subject: Stanislas' engine

Resent-From: nm

Date: Sat, 28 Mar 2020 14:53:18 +0100 (CET)

From: fl

To: Megill, Norman

Hi Norm,

Could you ask Stanislas how long

dors it take to minimize a proof

and would it be possible to launcher

minimize_with and Stanislas' engine

to compare the results. And I

guess the neural network must

be made again for each new version

of set.mm, so how long does it take

to train the network.

--

FL

Mar 28, 2020, 5:25:42 PM3/28/20

to Metamath

Hi Stan,

I had a look at the proofs - very impressive results! Especially because we had a global minimization recently, and your method found much shorter proofs nevertheless.

I had a closer look at the proofs for the theorems I contributed (these are theorems I contributed in my first year working with Metamath, so I was lacking experience):

* opabbrex: reduction from 12 to 7 essential steps, using ~ssopab2

* 2eluzge0: reduction from 5 to 3 essential steps, using ~nn0uz

* elfz0add: reduction from 16 to 10 essential steps, using ~uzaddcl

* elfzmlbm: reduction from 33 to 16 essential steps, using ~lesub1dd

* 2eluzge0: reduction from 5 to 3 essential steps, using ~nn0uz

* elfz0add: reduction from 16 to 10 essential steps, using ~uzaddcl

* elfzmlbm: reduction from 33 to 16 essential steps, using ~lesub1dd

Observations:

* the number of essential steps was almost halved

* the usage of only one theorem (indicated above) caused most of the shortening

* the proofs are still comprehensible, even better to understand because they are shorter

I would really appreciate if you continue your work to find more shortenings using OpenAI.

Alexander

Mar 28, 2020, 6:51:49 PM3/28/20

to metamath

On Sat, 28 Mar 2020 14:25:41 -0700 (PDT), "'Alexander van der Vekens' via Metamath" <meta...@googlegroups.com> wrote:

> Hi Stan,

> I had a look at the proofs - very impressive results! Especially because we

> had a global minimization recently, and your method found much shorter

> proofs nevertheless.

I agree. Any ML-based system is impressive if it can find many
> Hi Stan,

> I had a look at the proofs - very impressive results! Especially because we

> had a global minimization recently, and your method found much shorter

> proofs nevertheless.

*shorter* proofs the than ones we already have. Nice work.

I compared elfzmlbm - the biggest shortening - and I think the new proof

is quite readable. Its use of Z>= for example seemed quite clear.

We already run minimization runs and (usually) just accept what is shortest

(as long as it doesn't add axioms or other discouraged statements).

So this OpenAI minimization process easily fits into what we're already doing.

As a general rule, if someone thinks that a proof's readability requires reaching

certain steps, then those steps should be expressed as separate lemmas.

> On Thursday, March 26, 2020 at 5:24:02 PM UTC+1, Stanislas Polu wrote:

> > At OpenAI we've been exploring the use of deep learning for formal

> > math for the past couple months. We've worked a lot with Metamath

> > whose simplicity makes it very amenable to deep learning.

or even better, the models & supporting code that generates the proofs.

I'd *really* like to see the models :-) !!

Work to minimize existing proofs is great, but I'm hoping that this can

increasingly be used to create new proofs of claims that are not (yet) formally proven.

> > We're very curious to hear from the community on whether this is

> > useful. Additionally, if the authors of the original proofs shortened

> > by this PR have qualitative feedback on the proposed versions, we'd be

> > keen on hearing from them as well, obviously.

This is also revealing that some of our conventions aren't written down

and should be. Here are the documented conventions:

http://us.metamath.org/mpeuni/conventions.html

For example, we mention "OLD" and "ALT" but not why they might be used

and that they usually follow the "main" proof. I'll make a PR to fix that.

> > As mentioned in the PR the models were run on a sample of ~1k proofs

> > from set.mm so we could probably get 45 times as many shorter proofs

> > if there is interest for it!

In addition, I *suspect* that shorter proofs would be helpful for future ML

algorithms, because they'd be shown "shorter" ways to do it.

That later claim might not be correct; if "shorter" ways are always shown, an ML

model might only learn "specialized" techniques instead of general ones.

It might be wise to keep around a few of the older proofs that show more

general techniques, even if minimized, so that humans and programs will

have examples of more general approaches.

If you do that, I urge you to do it in batches to start with (instead of all at once).

That will let us review the results in part before you completely "turn it loose" :-).

--- David A. Wheeler

Mar 29, 2020, 4:59:19 AM3/29/20

to meta...@googlegroups.com, David A. Wheeler

Hi Stan,

Your results shortening proofs are very impressive, and very interesting!

I'd be curious to know whether you have to start from existing proofs,

or you generate new proofs from scratch. I assume you generate proofs

from scratch, but chose to work on existing proofs because they are

known to be provable?

In addition to existing proofs, would you also work on new proofs?

(there are several of them in set.mm, you can find them by searching for

" ? $. " or " ? @. ").

How would the AI behave if given a statement that cannot be proved?

(syntactically, or worse, semantically wrong)

BR,

_

Thierry

Your results shortening proofs are very impressive, and very interesting!

I'd be curious to know whether you have to start from existing proofs,

or you generate new proofs from scratch. I assume you generate proofs

from scratch, but chose to work on existing proofs because they are

known to be provable?

In addition to existing proofs, would you also work on new proofs?

(there are several of them in set.mm, you can find them by searching for

" ? $. " or " ? @. ").

How would the AI behave if given a statement that cannot be proved?

(syntactically, or worse, semantically wrong)

BR,

_

Thierry

Mar 29, 2020, 5:16:32 AM3/29/20

to meta...@googlegroups.com

Thanks Morman,

FL,

Proof minimization cost depends on how long we want/need to search.

For a small proof it can be minutes, for larger proofs hours, and for

some statements obviously we still, for now :), fail to find a proof

in reasonable time despite them being provable with available axioms

and definitions. We're happy to run our models on whichever

list/benchmark you'd be interested in.

Indeed, the models are trained on a particular version of set.mm, but

note that these models are not really impacted by small changes to

their training set.

-stan

FL,

Proof minimization cost depends on how long we want/need to search.

For a small proof it can be minutes, for larger proofs hours, and for

some statements obviously we still, for now :), fail to find a proof

in reasonable time despite them being provable with available axioms

and definitions. We're happy to run our models on whichever

list/benchmark you'd be interested in.

Indeed, the models are trained on a particular version of set.mm, but

note that these models are not really impacted by small changes to

their training set.

-stan

> --

> 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/83b9299e-c8ac-49d3-9393-2700f04e59bc%40googlegroups.com.
> 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.

Mar 29, 2020, 5:17:28 AM3/29/20

to meta...@googlegroups.com

Thanks Alexander for your analysis and feedback.

> I would really appreciate if you continue your work to find more shortenings using OpenAI.

That's definitely the plan :+1:

-stan

> I would really appreciate if you continue your work to find more shortenings using OpenAI.

-stan

> --

> 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/1c23b864-6b53-4ede-a2df-23851315e523%40googlegroups.com.
> 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.

Mar 29, 2020, 5:24:07 AM3/29/20

to meta...@googlegroups.com

Thanks David!

> I'm really hoping that you'll eventually publish 1+ papers about this,

> or even better, the models & supporting code that generates the proofs.

> I'd *really* like to see the models :-) !!

This is obviously the goal. The timing is still a work in progress,

but we will most definitely share our results formally with the

community.

> Work to minimize existing proofs is great, but I'm hoping that this can

> increasingly be used to create new proofs of claims that are not (yet) formally proven.

This is obviously the plan :+1:

> Well, I think you know the answer. It's useful, with stars and exclamation marks :-).

Your feedback as well as everyone else's is a very powerful validation

of our work internally and externally, so expect us to continue

pushing! Thank you.

> In addition, I *suspect* that shorter proofs would be helpful for future ML

> algorithms, because they'd be shown "shorter" ways to do it.

> That later claim might not be correct; if "shorter" ways are always shown, an ML

> model might only learn "specialized" techniques instead of general ones.

> It might be wise to keep around a few of the older proofs that show more

> general techniques, even if minimized, so that humans and programs will

> have examples of more general approaches.

Agreed.

> If you do that, I urge you to do it in batches to start with (instead of all at once).

> That will let us review the results in part before you completely "turn it loose" :-).

Roger that.

-stan

> I'm really hoping that you'll eventually publish 1+ papers about this,

> or even better, the models & supporting code that generates the proofs.

> I'd *really* like to see the models :-) !!

but we will most definitely share our results formally with the

community.

> Work to minimize existing proofs is great, but I'm hoping that this can

> increasingly be used to create new proofs of claims that are not (yet) formally proven.

> Well, I think you know the answer. It's useful, with stars and exclamation marks :-).

of our work internally and externally, so expect us to continue

pushing! Thank you.

> In addition, I *suspect* that shorter proofs would be helpful for future ML

> algorithms, because they'd be shown "shorter" ways to do it.

> That later claim might not be correct; if "shorter" ways are always shown, an ML

> model might only learn "specialized" techniques instead of general ones.

> It might be wise to keep around a few of the older proofs that show more

> general techniques, even if minimized, so that humans and programs will

> have examples of more general approaches.

> If you do that, I urge you to do it in batches to start with (instead of all at once).

> That will let us review the results in part before you completely "turn it loose" :-).

-stan

> --

> 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/E1jIKIt-0002k1-EZ%40rmmprod07.runbox.
> 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.

Mar 29, 2020, 5:29:45 AM3/29/20

to meta...@googlegroups.com, David A. Wheeler

> I'd be curious to know whether you have to start from existing proofs,

> or you generate new proofs from scratch. I assume you generate proofs

> from scratch, but chose to work on existing proofs because they are

> known to be provable?

These shortened proofs were indeed noticed as part of applying our
> or you generate new proofs from scratch. I assume you generate proofs

> from scratch, but chose to work on existing proofs because they are

> known to be provable?

prover on the test split we created from set.mm as we continuously

evaluate the performance of our systems. In that set up we only have

access to the statements.

> In addition to existing proofs, would you also work on new proofs?

> (there are several of them in set.mm, you can find them by searching for

> " ? $. " or " ? @. ").

> How would the AI behave if given a statement that cannot be proved?

> (syntactically, or worse, semantically wrong)

If the statement can't be proved, the system would simply search until

it reaches a timeout.

-stan

> 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.

Mar 29, 2020, 1:08:10 PM3/29/20

to metamath, Stanislas Polu

FYI, we have a short wiki page about automated proving for Metamath:

https://github.com/metamath/set.mm/wiki/Automated-proving

Expansions of that page are welcome. I put it in the wiki because that was easy to get started. If people think it should go somewhere else, please let me/us know.

--- David A. Wheeler

https://github.com/metamath/set.mm/wiki/Automated-proving

Expansions of that page are welcome. I put it in the wiki because that was easy to get started. If people think it should go somewhere else, please let me/us know.

--- David A. Wheeler

Mar 30, 2020, 5:19:29 AM3/30/20

to meta...@googlegroups.com

Benoit,

As a follow-up, our provers failed on both proofs over the weekend.

It was kind of expected for ~midexlem given its length and our current

capabilities; For ~mideulem it's also understandable given that it is

based on ~opphllem which is barely used elsewhere. In particular, if

the proof search misses ~opphllem's exact statement, it is as if it

had to prove it which is, similarly to ~midexlem, still beyond our

reach in terms of number of steps... for now.

I'll keep an eye on both!

-stan

> --

> 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/b1bab644-ea9f-49ba-8238-0377228266ab%40googlegroups.com.

As a follow-up, our provers failed on both proofs over the weekend.

It was kind of expected for ~midexlem given its length and our current

capabilities; For ~mideulem it's also understandable given that it is

based on ~opphllem which is barely used elsewhere. In particular, if

the proof search misses ~opphllem's exact statement, it is as if it

had to prove it which is, similarly to ~midexlem, still beyond our

reach in terms of number of steps... for now.

I'll keep an eye on both!

-stan

> I hope you can run OpenAI on more proofs. Looking at some the first shortenings, it looks like it can behave as a more efficient "minimize_with" in some cases where there are many "weakenings". For instance, ~mideulem and ~midexlem use a lot of weakenings in the form of adantr, adantlr, ad2antrr, simplr, simprl... Could you run OpenAI on these two theorems to see what it does ?

>

> Benoît

>

>

> Benoît

>

> 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.

Mar 30, 2020, 8:12:51 AM3/30/20

to Metamath

Very interesting work, Stanislas! Great to see the cooperation between classical AI (in the form of theorem provers) and modern machine learning.

I have several questions which I hope you could comment on.

1. Is your algorithm able to eventually prove any provable result given enough time? In other words, is the proof search exhaustive?

2. Does it work for any metamath database or only for set.mm?

3. Does your prover use facts it learned from the training set or it uses theorems from the database? I.e. if you were to change all theorem names in the database so they are different from ones used in the training set, would the model still work well? What if you "jumble" theorems (say, change order in conjunctions of clauses), will the model work better than a usual search or it will be ineffective?

4. Related to previous questions, can you transfer skills the model learned from one database to another? For instance, can it learn to prove intuitionistic theorems faster if it was first trained on classical logic?

5. Do you get (or hope to get) some sort of discriminative/generative model as a byproduct? For example, given a trained model, can you evaluate the probability that some proposition is true? Can you autosuggest possible theorems/steps to use based on your model? Clearly this question has proof assistants in mind :-)

I would also like to suggest some theorems for a test: if the answer to question 2 is positive, you could try your algorithm on quantum logic (see http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see http://us2.metamath.org:88/ileuni/mmil.html).

As for set.mm, it would be interesting to see how it behaves on calculational proofs like, for example, proofs that certain numbers are prime (see http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another interesting topic is proofs in the Tarskian geometry section (see http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly use propositional calculus and Tarski axioms, which reduces the search space. Geometric proofs also have some sort of "geometric intuition" behind them which may (or may not) be helpful for finding proofs.

I have several questions which I hope you could comment on.

1. Is your algorithm able to eventually prove any provable result given enough time? In other words, is the proof search exhaustive?

2. Does it work for any metamath database or only for set.mm?

3. Does your prover use facts it learned from the training set or it uses theorems from the database? I.e. if you were to change all theorem names in the database so they are different from ones used in the training set, would the model still work well? What if you "jumble" theorems (say, change order in conjunctions of clauses), will the model work better than a usual search or it will be ineffective?

4. Related to previous questions, can you transfer skills the model learned from one database to another? For instance, can it learn to prove intuitionistic theorems faster if it was first trained on classical logic?

5. Do you get (or hope to get) some sort of discriminative/generative model as a byproduct? For example, given a trained model, can you evaluate the probability that some proposition is true? Can you autosuggest possible theorems/steps to use based on your model? Clearly this question has proof assistants in mind :-)

I would also like to suggest some theorems for a test: if the answer to question 2 is positive, you could try your algorithm on quantum logic (see http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see http://us2.metamath.org:88/ileuni/mmil.html).

As for set.mm, it would be interesting to see how it behaves on calculational proofs like, for example, proofs that certain numbers are prime (see http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another interesting topic is proofs in the Tarskian geometry section (see http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly use propositional calculus and Tarski axioms, which reduces the search space. Geometric proofs also have some sort of "geometric intuition" behind them which may (or may not) be helpful for finding proofs.

Mar 31, 2020, 5:04:15 AM3/31/20

to meta...@googlegroups.com

Hi Savas!

> 1. Is your algorithm able to eventually prove any provable result given enough time? In other words, is the proof search exhaustive?

Theoretically yes but with very low probability.

We're not tied to set.mm in any way. I think we may have a few

assumptions here and there (eg. we treat |- as a special symbol in

some of our internal formats) but they can easily be removed.

> I would also like to suggest some theorems for a test: if the answer to question 2 is positive, you could try your algorithm on quantum logic (see http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see http://us2.metamath.org:88/ileuni/mmil.html).

How large are the quantum logic and intuitionistic logic databases?

What would be the main value of applying our proves on them out of

curiosity?

> 3. Does your prover use facts it learned from the training set or it uses theorems from the database? I.e. if you were to change all theorem names in the database so they are different from ones used in the training set, would the model still work well? What if you "jumble" theorems (say, change order in conjunctions of clauses), will the model work better than a usual search or it will be ineffective?

We don't rely on theorem names but statements. The statistical models

do memoize specific formulations of theorems and we rely on set.mm at

proof search to check that the theorem we apply are indeed part of the

database, proven, and not appearing after the statement we're trying

to prove.

> 4. Related to previous questions, can you transfer skills the model learned from one database to another? For instance, can it learn to prove intuitionistic theorems faster if it was first trained on classical logic?

Yes.

> 5. Do you get (or hope to get) some sort of discriminative/generative model as a byproduct? For example, given a trained model, can you evaluate the probability that some proposition is true? Can you autosuggest possible theorems/steps to use based on your model? Clearly this question has proof assistants in mind :-)

Yes. Not only theorems but also terms for unification as well

(otherwise we wouldn't make much progress in Metamath/set.mm). Do you

believe the community would be interested in an online tool to

discharge goals?

> As for set.mm, it would be interesting to see how it behaves on calculational proofs like, for example, proofs that certain numbers are prime (see http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another interesting topic is proofs in the Tarskian geometry section (see http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly use propositional calculus and Tarski axioms, which reduces the search space. Geometric proofs also have some sort of "geometric intuition" behind them which may (or may not) be helpful for finding proofs.

The model is capable to prove some of the prime number theorems, but

proofs sizes do grow very fast. I believe we already proved 17 as an

example. Out of curiosity, why are you specifically interested in

these two classes of theorems?

Thanks!

-stan

> --

> 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/353a6707-14fd-4c08-a6e6-611972c84916%40googlegroups.com.

> 1. Is your algorithm able to eventually prove any provable result given enough time? In other words, is the proof search exhaustive?

We're not tied to set.mm in any way. I think we may have a few

assumptions here and there (eg. we treat |- as a special symbol in

some of our internal formats) but they can easily be removed.

> I would also like to suggest some theorems for a test: if the answer to question 2 is positive, you could try your algorithm on quantum logic (see http://us2.metamath.org:88/qleuni/mmql.html) and intuitionistic logic (see http://us2.metamath.org:88/ileuni/mmil.html).

What would be the main value of applying our proves on them out of

curiosity?

> 3. Does your prover use facts it learned from the training set or it uses theorems from the database? I.e. if you were to change all theorem names in the database so they are different from ones used in the training set, would the model still work well? What if you "jumble" theorems (say, change order in conjunctions of clauses), will the model work better than a usual search or it will be ineffective?

do memoize specific formulations of theorems and we rely on set.mm at

proof search to check that the theorem we apply are indeed part of the

database, proven, and not appearing after the statement we're trying

to prove.

> 4. Related to previous questions, can you transfer skills the model learned from one database to another? For instance, can it learn to prove intuitionistic theorems faster if it was first trained on classical logic?

> 5. Do you get (or hope to get) some sort of discriminative/generative model as a byproduct? For example, given a trained model, can you evaluate the probability that some proposition is true? Can you autosuggest possible theorems/steps to use based on your model? Clearly this question has proof assistants in mind :-)

(otherwise we wouldn't make much progress in Metamath/set.mm). Do you

believe the community would be interested in an online tool to

discharge goals?

> As for set.mm, it would be interesting to see how it behaves on calculational proofs like, for example, proofs that certain numbers are prime (see http://us2.metamath.org:88/mpeuni/mmtheorems145.html#mm14463s). Another interesting topic is proofs in the Tarskian geometry section (see http://us2.metamath.org:88/mpeuni/mmtheorems237.html#mm23691h). Those mostly use propositional calculus and Tarski axioms, which reduces the search space. Geometric proofs also have some sort of "geometric intuition" behind them which may (or may not) be helpful for finding proofs.

proofs sizes do grow very fast. I believe we already proved 17 as an

example. Out of curiosity, why are you specifically interested in

these two classes of theorems?

Thanks!

-stan

> 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.

Mar 31, 2020, 6:27:57 AM3/31/20

to Metamath

How large are the quantum logic and intuitionistic logic databases?

What would be the main value of applying our proves on them out of

curiosity?

Quantum logic database is ~560KB, intuitionistic logic database is ~3.7MB. Trying out your prover on the quantum logic would be interesting because of how different it is from usual logic. Also typical proofs in that database seem to be smaller than in set.mm, so perhaps your algorithm has a higher chance of coming up with proofs in quantum logic.

As for intuitionistic logic, I was interested in how well the model trained on set.mm would transfer its skills to iset.mm. Also many theorems from iset.mm have their set.mm counterparts, so theoretically you could contribute to iset.mm by trying to prove some existing set.mm results in the intuitionistic setting.

As for intuitionistic logic, I was interested in how well the model trained on set.mm would transfer its skills to iset.mm. Also many theorems from iset.mm have their set.mm counterparts, so theoretically you could contribute to iset.mm by trying to prove some existing set.mm results in the intuitionistic setting.

Do you believe the community would be interested in an online tool to discharge goals?

I think others are in a better position to comment on this, since I haven't formalized anything in quite a while. Personally, I would really like to see a Metamath Solitare kind of tool which would autosuggest you steps based on your model, just to explore how well it works in pair with a human operator.

The model is capable to prove some of the prime number theorems, but

proofs sizes do grow very fast. I believe we already proved 17 as an

example. Out of curiosity, why are you specifically interested in

these two classes of theorems?

Basic arithmetic results are interesting since you can easily generate many "theorems" of the form "12 + 29 = 41" and you can even roughly estimate

the amount of steps such theorems should require. Proving these identities is a purely mechanical task (as far as I remember, Mario even wrote a program to do that), so it's interesting to know whether your model can learn to perform such a feat.

As for Tarskian geometry, results in that section use a relatively small subset of set.mm theorems and have an underlying geometric intuition. In my opinion it's interesting to evaluate if your system performs better on geometry theorems rather than on propositional calculus/set theory results. Also, elementary geometry section has a collection of results with statements but without proofs (marked by "? @" and "? $.", as mentioned by Thierry).

the amount of steps such theorems should require. Proving these identities is a purely mechanical task (as far as I remember, Mario even wrote a program to do that), so it's interesting to know whether your model can learn to perform such a feat.

As for Tarskian geometry, results in that section use a relatively small subset of set.mm theorems and have an underlying geometric intuition. In my opinion it's interesting to evaluate if your system performs better on geometry theorems rather than on propositional calculus/set theory results. Also, elementary geometry section has a collection of results with statements but without proofs (marked by "? @" and "? $.", as mentioned by Thierry).

Mar 31, 2020, 6:55:18 AM3/31/20

to meta...@googlegroups.com

> As for intuitionistic logic, I was interested in how well the model trained on set.mm would transfer its skills to iset.mm. Also many theorems from iset.mm have their set.mm counterparts, so theoretically you could contribute to iset.mm by trying to prove some existing set.mm results in the intuitionistic setting.

Very interesting. Arguably higher level theorems proofs would
eventually become ~~ similar?

> Basic arithmetic results are interesting since you can easily generate many "theorems" of the form "12 + 29 = 41" and you can even roughly estimate

> the amount of steps such theorems should require. Proving these identities is a purely mechanical task (as far as I remember, Mario even wrote a program to do that), so it's interesting to know whether your model can learn to perform such a feat.

> As for Tarskian geometry, results in that section use a relatively small subset of set.mm theorems and have an underlying geometric intuition. In my opinion it's interesting to evaluate if your system performs better on geometry theorems rather than on propositional calculus/set theory results. Also, elementary geometry section has a collection of results with statements but without proofs (marked by "? @" and "? $.", as mentioned by Thierry).

-stan

> 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.

Mar 31, 2020, 7:12:46 AM3/31/20

to Metamath

Very interesting. Arguably higher level theorems proofs would

eventually become ~~ similar?

Mar 31, 2020, 8:59:50 AM3/31/20

to Metamath

"Do you believe the community would be interested in an online tool to discharge goals?"

Personally I think an AI assisted proof tool would be really cool.

I also think it could be really helpful for getting new people into MM. If there were a dozen easy problems people could do to start going, like Filip's ones which are nice, that would help beginners I think. Then when trying harder things the AI could make suggestions or offer to finish the proof when they are close.

Mar 31, 2020, 11:46:06 AM3/31/20

to meta...@googlegroups.com

There's a general phenomenon in which you can have statements which are not equivalent in iset.mm but which become equivalent given excluded middle. Examples include inhabited versus nonempty, the two sides of http://us2.metamath.org:88/ileuni/xorbin.html , apart versus not equal, and others. The rpneg vs rpnegap example illustrates two of these - apartness and exclusive or. There's a whole section http://us2.metamath.org:88/ileuni/mmil.html#intuitionize about how to turn a set.mm proof into an iset.mm proof.

I wouldn't say that higher level theorems are necessarily more similar than lower level theorems - see for example the discussion of the intermediate value theorem in http://us2.metamath.org:88/ileuni/mmil.html#Bauer . Or any number of theorems about series convergence (which I don't know off the top of my head, but there is a bunch of stuff about modulus of convergence and such).

But I think the "would
eventually become ~~ similar?" question wasn't about "similarity"
in a general sense, but specifically about double negation. I'm
not sure I have anything to offer on that. A metamath.exe run of
"search * '-. -.'" in iset.mm shows almost no hits, nor do I
remember much of the literature I've been using talking about
double negation. I've seen things like
https://en.wikipedia.org/wiki/Double-negation_translation but
haven't tried to formalize anything described there. Nor do I know
how it applies to set theory - that page stops at first-order
logic and Heyting/Peano arithmetic.

--

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/aed41439-97b7-48c9-aba0-3fbbfa1a942e%40googlegroups.com.

Reply all

Reply to author

Forward

0 new messages