My current progress here: https://github.com/metamath/set.mm/commit/4ea74c3d42b6f6fc8087b9fd2323285dedf76869
So far, I made almost all proofs by hand (in metamath.exe) without any help. The only exception is ~axk4, where after making a number of unsuccessful attempts I quickly peeked at Boolos book. I have the impression that there is basically only one idea that derives ~axk4 from ~ax-gl, and if you don't find that idea then you're lost. Interestingly, the proof is pretty short once you get the right track. Some of the long ones were not easy too, but I got them in the end. I have not compared my proofs with the ones in the book (except for ~axk4), so maybe there are original ideas in here. -- 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 visit https://groups.google.com/d/msgid/metamath/94c0fdc6-74bd-460d-abbc-ecd05a104243n%40googlegroups.com.
