Deep Learning powered proof shortening

[Stanislas Polu]

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

[Benoit]

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

[Stanislas Polu]

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.

[OlivierBinda]

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

[Stanislas Polu]

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

[Jim Kingdon]

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

[Dirk-Anton Broersen]

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.

 

[Benoit]

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

[Dirk-Anton Broersen]

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.

 

[Benoit]

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.

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.

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

Benoît

[Benoit]

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

[Stanislas Polu]

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.

[Norman Megill]

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

[Alexander van der Vekens]

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

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

[David A. Wheeler]

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

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 :-) !!

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.

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

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!

Yes, I would certainly like to see that. Shorter proofs tend to be easier to understand.

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

[Thierry Arnoux]

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

[Stanislas Polu]

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

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

[Stanislas Polu]

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

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

[Stanislas Polu]

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

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

[Stanislas Polu]

> 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
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 " ? @. ").

This is a great idea.

> How would the AI behave if given a statement that cannot be proved?
> (syntactically, or worse, semantically wrong)

We check the syntax of submitted statements against the wff grammar.
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.

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/531b6980-d1ba-e90f-a47d-c0830bc709cb%40gmx.net.

[David A. Wheeler]

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

[Stanislas Polu]

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

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.

[savask]

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.

[Stanislas Polu]

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.

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

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.

[savask]

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.

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

[Stanislas Polu]

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

We have and leverage proof generators for a number of these tasks :+1:

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

Good to know, thanks for that!

-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/10f37787-f926-4989-9adf-a3daf972acdd%40googlegroups.com.

[savask]

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

I think so. For example, compare rpneg from set.mm and rpnegap from iset.mm - they are certainly similar but not the same (maybe Jim could comment on how well proofs of high-level theorems translate from set.mm to iset.mm).

[Jon P]

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

[Jim Kingdon]

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.