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.
