A < B -> A and B are real and it's use in theorem statements.

[Jon P]

I've been playing around with the OpenAI assistant too, thanks so much Stan and Auguste for letting me use it. It did something weird the other day which was surprising to me and I imagine everyone else knows this already but I wanted to ask what to do.

It proved this ( A < B -> ( A e. RR* /\ B e. RR* ) ) as part of a proof, which I found surprising. The main idea is < is defined on the reals, ltrelxr.

And so I have ioounsn in my mathbox which is stated as ( ( A e. RR* /\ B e, RR* /\ A < B ) -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) ) but using this trick above I managed (well mostly the assistant managed) to prove ( A < B -> ( ( A (,) B ) u. { B } ) = ( A (,] B ) ), here is the proof.

So I guess my questions are firstly is it good form to reduce the number of hypotheses? Does this have implications for other proofs in the main body such as xrltle or it's nearby theorems. I think there must be a lot which state A e. RR* /\ B e. RR* as well as A < B in them. I guess it doesn't matter because A e. RR* isn't constricting the theorem at all, it's just a redundant statement so maybe it is irrelevant. I am not sure if anyone else is interested but I thought this quirk was cool.

Also as a side note is it ok to upload deduction versions of the theorems in my mathbox? I don't want to have too many copies of trivial things in there. It's a bit hard to replace what I have as I've already used them in later theorems, though maybe changing them too is not insurmountable.

[Alexander van der Vekens]

That's really cool: I think you are right with your assumption that the number of hypotheses should be as small as possible, and ~xrltle could/should be revised accordingly (in my opinion).  Unfortunately, I cannot see your proof for ( A < B -> ( A e. RR* /\ B e. RR* ) )  (the link goes to a site for which I have to provide login information), but I guess you use ~brel to prove it.

Of course such a change will have an impact on existing proofs - they should become shorter.  ~xrltle is currently used 65 times. I do not know if the minimize command will replace the current version as soon as the new version (without hypotheses) is avaiable.

[Jon P]

Awesome, very interesting. My concern is there are a lot of candidates in the database which have this type of structure. You are quite correct re brel, here is it's output:

⊢ ( A < B -> ( A e. RR* /\ B e. RR* ) )

    0.91 brel

    ⊢ < C_ ( RR* X. RR* )

         1.00  ltrelxr

If you are interested in the tool Stan talks about it here and his email is in the intro pdf if you want to get credentials. 

I'd recommend it, it's really interesting to play with and eventually it will take over from humans in mathematics so it's worth trying to get on it's good side while we have the chance :)

[Mario Carneiro]

This fact was being deliberately not exploited, for reasons that I forget, possibly involving type hygiene or something. I think Norm made the call on that so perhaps he can recall better.

Mario

--
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/24949dad-3d5b-4a94-b5e4-4d8c01ff74b7n%40googlegroups.com.

[Mario Carneiro]

Found it:

https://groups.google.com/g/metamath/c/2AW7T3d2YiQ/m/iSN7g87t3ikJ

[Jon P]

Ah thanks Mario, yeah all of Norm's points make good sense.

[Steve Rodriguez]

I had noticed, and in a few proofs like nzss used, the similar reverse-closure dvdszrcl of the divides relation.  That has been used by a few others' theorems too; not sure if that's as much a problem as the less-than closure here, in which case...oops?

Steve

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

[Stef O'Rear]

On Tue, Aug 11, 2020 at 3:48 PM Mario Carneiro <di....@gmail.com> wrote:
>

> This fact was being deliberately not exploited, for reasons that I forget, possibly involving type hygiene or something. I think Norm made the call on that so perhaps he can recall better.

This is one of many reasons I'm uncomfortable with metamath's recent
"pivot to AI"

-s

[David A. Wheeler]

On August 12, 2020 2:01:43 PM EDT, Stef O'Rear <sor...@gmail.com> wrote:
>This is one of many reasons I'm uncomfortable with metamath's recent
>"pivot to AI"

I, for one, welcome our new artificial intelligence overlords :-).

To be fair, there have been metamath efforts using artificial intelligence for years. Artificial intelligence has been involved in theorem proving for many many decades.

I don't think there's anything to be uncomfortable about. Humans still need to decide what the axioms are & what is worth proving.

Perhaps the lesson is that if we want certain conventions to be followed, we need to express them so that they can be automatically enforced. The "discouraged" marks, for example, can help do this. I think that is entirely in keeping with the overall approach of metamath.. everything to be explicit and automatically verified.


--- David A.Wheeler