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 <https://docs.google.com/document/d/1cpbz2ZJ60qR0220fUTvCWAv4NYX4y8JTClCwGnzryXc/edit?usp=sharing>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.
