I managed to prove ax3 from w2 manually! (append this to ./data/w2.txt to verify)
[15] CpCCNqqq = D[11][14] % Axiom 3 [16] CCNpNqCqp = DDD1[15]DDD1DDD1DDD1[15]DDD1[14]1[15][15][8]11[15][15] Based on how procedural/repetitive this manual proof looks compared to the more brute force proofs, there’s probably a shorter proof of this. I found this manually-ish by looking at random pmGenerator proofs and only filling in steps that require lots of syntax to match. Doing this generalizes a pmGenerator proof to an inference proof. Unfortunately due to inane reasons my desktop computer doesn't have internet but I took relevant photos Details: Letting w2 be 1, a1dt (frege24) be 2, luk2 be 3, partially proving DDD1DD2DD1D233321 in metamath.exe resulted in w2-q, which I then repurposed for ax3 I think proofs with hypotheses are more intuitive for humans, but I’m not sure how much this can help computers. I tried to send photos of my metamath proofs but for some reason each photo is like 8 mb and gmail refuses to send that long of an email. I posted them to https://github.com/icecream17/Stuff/blob/main/math/ <https://github.com/icecream17/Stuff/blob/main/math/IMG_0057.jpeg> and the files are in the format “IMG_00xx.JPEG” -- 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/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com.
