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 
<https://mmproofassistant.azurewebsites.net/#eJyNU91vmzAQ/1csPzUTySAMRlA0aaEvq1Rp4qlSGk0GnGDi2gxM2izjf5/Nx+w0S7QHpLuzud/H+U6QCPxSw/AE3/iiCNxEUJWIY4lhCClKMIUWLFGFmYAhayi1YC2Q/KkrQCrIS1lheYdkMtVNLEg5ygjbwXCLaI1bC+6zgnxaBIeDgZDhOq1IKQhnN3HuIs5ERZJG4AwkR/DAGfiOGUNMWMCbPjR0Orfn9mwyMtFgErkuXbHIqG8i58eSixzXpL4JPPbTLfrzRpoGU8prnCmEw3afp/ucZQbCjqPb5t2Br2AJVmD6BagQz0AcfwAfn59lbUgmYHJhpQVTTikqFfRY6ThqEgZHXmKmGDpkFxQ/X18Lg6FAqSCpwfGixUh1vQa/pyAG0Q9JNQJPM3AvuW02qqq4x2cyIi1CXZuA00kehPJrWxWvZLwa4kjGSmmf3Z9lscyWMlYWdE8xhEnVvchOr5b0Xq8cCKKNlGjPFnbgO599d+54dhDYvrTC9ci2EL4rrg/rovdoxLK3QHF8Gkb0/wPSwP8YkOc5/v4XSfObA3rfwhhQP40rBAf7qJD+vVWjgxrzqoNO26rfj7yRMOuzDdc7Zp3th/mITB9N7hp5Yw0yv7Gy+bsnZcX59vGxT9s/lAtvBw==>
 ( 
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 
<http://us.metamath.org/mpegif/ltrelxr.html>.

And so I have ioounsn <http://us.metamath.org/mpeuni/ioounsn.html> 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 
<https://mmproofassistant.azurewebsites.net/#eJzNW22P2roS/isRn+CK3Zv3l9X2SrD9co901HbbqpV6qlVIAgTyAiQBkp7+9+u8euIYQ1h6T1WpskN2/Iyf8cx47PwYuLHjR4OHH4NjaKx0aRZ7eSdON87gYeCZM8cbjAcbc+cE8eAhSDxvPIhiE/1R8WDghmESRIEtordcGz3AYsYDLzRtN1gMHuamFzk/x4O1vXJlQ9/vwRi2E1k7dxO7YcAcafgUBvHOnSWxY3OzlPsjDLj3ThCYQTzmlLs/Eu9O5EX+flQjwYOhkffz9dJaLwMbjLwITbZyQ26z5O7+ww3Rvwk3HI+4KTfiknvuB2r8RM031Q/fix9GHZXHAyv0PHMTOXbzpMCG4ZQjJoiCQbhxghxrrPPLWDxoAcC6TDdhvHQiN7oI8YR7zCHVU4ElguEsL8xxoQEFU0gDJdiIYMDYtGLXAoN1MNdjfvvG/X3H4ZHfFJMBHk3Royf06Pt38sX86Y8fqPlweo5//sxfeSpewXNdPkWSHvL/yt6UJmaIGt9qgtCLOUeFVT8MnG28s+spwnNAMoKMx/QSNCf8vaQKgqLJsqDpvKKoMpq7TFBlzZGzxWnD6sjuZV9MfXqYHAZKMbnoYEeaw/viLbVoQ716rWBsFODp3HJsd3UwmaZL6s423badDpHtIWUmlQpFp9SostySLGiCWG3SeEdU4wU2mQTOVmyMEmvHMEpZ52VNlxRZlDRJkKTcg6SbuRk4icmgk5RN0lmq9abN4uWsYQgU1mTLsldaGgdM1kgRfVjLfc4EeheSkynBHJUNZ2uFfsMGRs1gw1B5STF0SVVUQRJFAWm7ne1nlmXJMYMNUnZ3cWEF3tT+4XI2MAQKG+ousHcB8uxMNkgRdDY2UeP7o7xvLTvUFI/QjFtLgpg3JwgpehHqTTnnnnt+/lebpCj1aoawJiyGdElQRF1FLAmSJuQM7RNt7QpKKy8hGSJlY4YaWK/nCQOh8BTaibu2j6bNDtOECMBTzcOkBXhSAJ5UgCdF4KmWzbQ9065luc1qwGhOznU+tbPgKKy2XjBjgiZ9/FnjwpYE+nHTL8zv33/9hRropbxR/DYq3jI7Jlk86tgceno2oWhHNWCrYJbz4afUTv0XxVIoc7Zq6GUx+48vJAXI2AXRDKyaBTy9DItXROSKkENCWYsmaHweIeTFIlYsP0kYFk/K7vqki1TsYf4YFcX8HVM5OI6asdzoOcjVlPaAhEelZeqzuSYG1mJ3FaThpTNYGnJpH+VPpRalPf+qvAsrR4sZfJJGSRYf2BGcENHonkM6cEcu5TJuNOKGOeR2/4nov0P9svW+aX1oWs+tdz+2ep9avc+t3pdGwteyVTqcd8WsHWsGxugvqubfRWaUNd3itWf0IOclQyOn+aIu3dD7flI+NVI+QylDbtg2jAM2jCrgfELPHlH77h41Pla8oz/9cK0aHQCHk2b6RKAZVhDKF78WWzz0wwHJfKpxsQ2f1C9/90sjMdd1VOZ9z0UT+3K22KfuevpC4AQDvoOL6X31a7mUPlS9KkZOQEI5BQl/3X6XB4Nx7enfo16+Nsveh+K3uveMeo9V+yNof8rbL1XnM+x8AW99hT8cUCer2kfUPlbtFLXTqp2hdkIE+OMxCZpkqlnijNCiy2j7ociaqmuGpmrIM5grZS7NopnOyqUI0Y1fGI/OmGzSNtlH9CBnMEGtymQvd3AYKcXBeXtzryWb3foKNXKC+6nxgvV46a8IxkpRhLf8Nb87HFlh8yQfpO/JOr4H4c1q55OVVac+0DE6CnQ9XXjifiX4V5lSXw5eRQGGStFDW678WPZn6ZUUZCed2rTjK7NuloB+yZqM4XKVMGqKSlvZlpdHXmTumBgqnfbTpIl1Ep+s9v+PRbPPLrgBTatJ6OnaiISdwMxoSJ8BMpomr8A7rbPuLCNtsI7AjTvr6cHt+Z0bhk3FotGJuUeT/VUki2rGLqKRXoap+nkXSKr+gnV/eYXyVrM1wloxlU9SL4y3M9lnKk/6Kcqu+pRRj+q9UrEEK1eJGsWWu7XVrtOIrK3Wcec5gRfXemHA7I333FrFVqpaTL1Iv3XGnvuSehtOQ7zdbZRi6q5mByEys1BlV7QId9CDU3rmSziqJ+yoLsoYu7THnhPvmnysUYqp+97V9qa+X7IPc0jnTi+4tKp43cJ4U2Upiiv4vbqikdUFjKa2cmEsA3WU7JKqiGmbATjLwVPAyFw1lLFKgiyroiHymqyjqfN1XbP5ucjK+UjZ18XpUqsrAzOGSQljgryzt0YUsjfmpAiS/oLjHHhRciPruPDXDv24sttVElhCM1f0+i6gm1bzlQrGpZpwrDSr7quJMuJbEWTV4GUlP7wLI9vfWFuBcSrckX2e8FtwjJFRODZi3tQ03QiZHJMirgpZpQYTXHCqfFhG+LCO36qpwViZXktQlTmvLII1UyWyPviKMjHpyypTbleLa1smDJNyNDG53HRXltnYbaM101HpqiDzMnJWhqHLKpqtQxxm6fZgGSy7JWR3rwjUZF9ulXhc2i5nK5iqG8fCK0BNrwCFx6Vt42eGkonL8orL/xEUHpe2JV/w21RKA3bKSU42I0RXltuN0cVSuMqK4ZmD62+8Jrhi8CxfK2qSguxWM1B4lfXcZueHzBMifcZigpR96YlDL9eKgVCoOXqubluZtGBSQ4q41VnoKe0YhD1STohqqrAyrAqezhuGwou6KEi8ouaHQ1kQKYkaH1m3QUjZmKomatyELYyFwpatSoKwjiOZffuDENFm65l7einudXy9594CgvL6MlTjCSvx9pJsHi+0t61eXeUFlM12TsMZVom1vGRdUGSZV2SDl6TiHpLvxkbmrXZzBmek7HoiHsspyDF+7e3p8MAUgubH7HCMfHXPzkYJEZ1M5QTAavq8GM3fsdkn4TGZGYeoHuauNre27H0SEVyuccKtRf4aJ4x3OBh8PyfMu4dYEdM5ywmTsn+JE8ZAaIeLc4NXFV9lX0ghRfRIBk8nf1dnfYAqkOBhTVgeWNEUUURuWFMkVdXznajsqkdL9A1m5ZuQfYsED49LocV1Asl1JXX1ClDX5FJ4XNp+17fTpaFpN7aVfyZgY2XOB2zFkHlVkgUDTcIqiNeBFoUscyFl/6qAjbHQ4sEqNUwtlFwmW6SI3zpgY5X6Bey1PzNWx/nCY3BGyr5JwMYDUwjazbdSIrqawiSIFPG6gI3HZAZsQ1zq+yzW2EVd8r7ObVb6tFPJ7HkzEYNnrWxNkhRFFzVD03ldyVe26lu7XSR4S4aVkLJv4XPxuNT4fNQXnhqxrj2dBgWvS/a/j4XHpgBbi5nirxRHYpoIKeLMDcmi+AXuEnfLXQ6+FYkRMG3Zmq2C41Kz2FGLJOE3ST4x+H7JZ5KstslGnlkMsyFl/5LkEwOhXTrYbmapo/vs4iop4jdNKLAy/SoAwtpcqta8dYpAUkXK/lUJBcZC+/4jMebH1DywTzl7s/UPbBWwJv22ClIW8+tD7LPOMEjZt9gq4HEptCyX+s4VNYt1vfgcqGvCFh6XAso3g5Wo2pHHtBXS3H7r5BOr1C/51BaGHobRnvXVGin7JsknHpiWfAq24CzDzYZdkiFEvDL5bMZkBOz8IMFMwwQN8631hSv+xnTc+sgSfisJv5uDH6LBD7Dgp07wUyD40Q38AAV+5NH6EAN8RwEvnsODM3jcAc8YYPEdFrhhpReWUmE1EVbwYP0Nls9gXQnux+HGFO784OYHbjjgdgGWG2DtApYM4FEM3B3ADBVmWjAFgYEDxjvoJOA6gbYJLQv6Oug4ob+CaSlMI+ElenilDl5Fgxe94D0teAcKXmGCd4jgFSB4vwZeEYG3HuDdAXg4Ds+b4akvvGaD77B8H1dL+7/BJl9X5bfMm10Yzv/8s+z+/B9p9hyj>
.

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 <http://us.metamath.org/mpeuni/xrltle.html> 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.

-- 
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 [email protected].
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/6b15581a-2090-43dd-bea0-c5723335b69eo%40googlegroups.com.

Reply via email to