Also note that our models are still not very good at these kinds of expression manipulations / basic algebra (there are not many of them in set.mm).
But we're working hard at making them much better at it. Will keep you posted when we update the underlying model in that direction. Best, -stan On Sun, Jul 19, 2020 at 2:08 PM Stanislas Polu <[email protected]> wrote: > > Hi Jon, > > Here's a proof for the A=1 part. The other part should be similar. It's a bit > tedious and you need to hint the model on a few eqtrd. I also had to hint > `mvlladdd` to it by doing a search for it. > > Hope it helps! > > -stan > > > On Sun, Jul 19, 2020 at 10:57 AM Stanislas Polu <[email protected]> wrote: >> >> Hi Jon! >> >> I think eqtri is at least a plausible way to go here. >> >> I think something along these lines could get you there? I entered the first >> eqtri manually here as the model fails to make useful progress early on. >> >> https://mmproofassistant.azurewebsites.net/#eJydV9uSojAQ/ZUUT1qDbiDIxap9UJ92q+YLZueB6xjuEmBE13/fgEIiIqvWVE2FDNPndJ/TnXAUcO5GRFgehX1i+Dqy8rB+yKvUFZZCaFpuKIhCamZunAvLuAhDUSC5Sf+p2RCiapZmSeLRl7BDn1kUUQgT08Hxl7D0zJC4J1EIHB8rhl6WHITjEjvDaY6TeBRoskniPMNWkbsOsCoggsXsdxHOZCjD+bSFZwgUjqQoN5xQ5eG2VZrkW5dgMoq2Au4cbDZtWBbp/FpBKyYkqRvXMKUXbO1gGzsczFdijtdtAlbgJ5DAjz9/wJquZDC9qZgo2EkYmilxnW6nocMQB+iQnSWnplkYz2e97mXdRRqAcQ0j0mB2cJ+HqXN/o1lPad6oBWPxBsB2FQmlg6fkr4BNAAL7OcWcUtQJrTR9qMFreK2FZwgD8FIi6Xak7hEHn5t2jm0O+kaVlsHHB/g7A+m2+U3A52e9mNQbtfh0ZwqOx/pxefHE6dRsELpxtsbpVHuj6cWlkEZoLuOWN6PW502NaYYFpQrnECqqApGsaCoyVGUBNZpUluulISsL/b5tb6Kz9qA8H/crgxooLgpI6GF5O9I+d3k05XmcB4Ma4CFj0yPld/Q1KnI/lWuR67qs60VNbHORetWsqaKrRuGzuhu6bpVe0/UEaGDWupM1SP1zpb67o0OwFZ9RHhNfliUVSoZiIEPXDaggmqznB3YWBAtppOj96Lz49+k+rgbjMKCGgwMf+gmBLxAcqeVTtmUcBgjGBYx3qPTgqF36Ifp2aebt2TDdcsOWE7r/Rjdq4qtucqzA7DI9O1tpV1a6Sfzac5ydSGGZjpPhzlIsrRFLIU2XEISSpC00SUe6Suth+8VeSv1oNyJYP3hbDa07dx5UhoENWWcfJS4OUvUFJgO1e5IaQx90tR99RxgaL1CTnmbSgQ0w0SzV+TYNXL1UpIEyvVFrtSfqgwQZhwGCpozzA4qxNdpf/RDPjuORVPiGuryEen/cXDrv3nxmOYw0k6Ip9FyWJWgodE7LqkKTVzwjLHFcpiPq9IM/pM5tKo/LxUgNyAUr4oXlYT82r//LGL3mI4Z9Q+xUK1MlBYX5uPo2YR8K4vXtnrvz8ldS/n7IX/T4mwl/N+DPJv6g4w8Evr/4icaPEL6JebPzteSF4WvBrjuf4qV3fsVp0V2Tmw+39/fz4+kfOGw5mQ== >> >> >> On Sun, Jul 19, 2020 at 10:28 AM Jon P <[email protected]> wrote: >>> >>> Hi Thierry, >>> >>> That's is very nice progress! I have been playing around with the tool and >>> I like it, it seems to have an obsession with eqtri however that also seems >>> to work out quite often so it's probably right to think highly of it. I >>> have done all the practice problems and I'm searching for some theorems I >>> might be able to prove with it. >>> >>> One thing I noticed doing Filip's practice problems is that the 4th problem >>> of his is much more difficult than the others and I have not yet been able >>> to solve it using suggestions from the tool. I found this a bit surprising. >>> My solutions are here if anyone is also trying the practice problems. I >>> don't know if anyone else has found anything similar. >>> >>> -- >>> 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/50a189c7-3f29-40ef-bd32-ee6246c2eceeo%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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACZd_0ytFwhg8gsx9T77M9OCtd8%3DfdNnBgnH4jOE-jBtxeX7Fg%40mail.gmail.com.
