By the way, proof compression further improves it to 1877 steps:
$ ./pmGenerator --transform data/w2.txt -f -n -t
CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -p -2 -d -z -o data/w2-z.txt
Wed Jul 10 18:28:49 2024: Process started. [pid: 26064, tid:1]
Tasks:
1. recombineProofSummary("data/w2.txt", true, null, 2, 18446744073709551614,
true, false, "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true, 18446744073709551615,
134217728, true, "data/w2-z.txt", true)
[Main] Calling recombineProofSummary("data/w2.txt", true, null, 2,
18446744073709551614, true, false, "CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true,
18446744073709551615, 134217728, true, "data/w2-z.txt", true).
0.14 ms taken to obtain 67 helper proof candidates, i.e. the minimal set of
referenced proofs such that each proof contains only a single rule with inputs.
19.61 ms taken to morph and parse 84 abstract proofs.
0.04 ms taken to validate 17 conclusions.
0.03 ms taken to find 5 occurrences of 5 theorems.
[Proof compression (rule search), round 1] Started. There are 27816 proof steps
in total.
[Proof compression (rule search), round 1] D-step [16] improved from D[79][15]
(1+2829+471 = 3301 steps) to D[79][74] (1+2829+115 = 2945 steps). [CCNpNqCqp]
[Proof compression (rule search), round 1] D-step [77] improved from D[75][15]
(1+1883+471 = 2355 steps) to D[75][74] (1+1883+115 = 1999 steps).
[CCNpNqCCNpCCNrsqCrp]
[Proof compression (rule search), round 1] D-step [57] improved from D[51][15]
(1+1367+471 = 1839 steps) to D[51][74] (1+1367+115 = 1483 steps). [CpCCNCpqCpqq]
[Proof compression (rule search), round 1] D-step [48] improved from D[37][15]
(1+421+471 = 893 steps) to D[37][74] (1+421+115 = 537 steps).
[CpCCNqCCNrsCNCpqCpqCrq]
[Proof compression (rule search), round 1] Complete. Applied 4 shortening
replacements.
[Proof compression (rule search), round 2] Started. There are 19272 proof steps
in total.
[Proof compression (rule search), round 2] Complete. Applied 0 shortening
replacements.
There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 11).
There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
There are 417 steps towards CCNppp / CCN0.0.0 (index 14).
There are 1877 steps towards CCNpNqCqp / CCN0N1C1.0 (index 16).
0.01 ms taken to count 2439 relevant proof steps in total.
0.02 ms taken to obtain 84 referenced indices.
0.03 ms taken to obtain 18 dedicated indices.
0.05 ms taken to build transformed proof.
0.63 ms taken to print and save 1129 bytes to data/w2-z.txt.
Wed Jul 10 18:29:05 2024: Process terminated. [pid: 26064, tid:1]
$ ./pmGenerator --transform data/w2-z.txt -f -n -t
CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -j -1 -s
CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq
-d -p -2
Wed Jul 10 18:29:08 2024: Process started. [pid: 23984, tid:1]
Tasks:
1. recombineProofSummary("data/w2-z.txt", true,
"CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq",
4294967295, 18446744073709551614, true, false,
"CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true, 18446744073709551615, 134217728,
false, null, true)
[Main] Calling recombineProofSummary("data/w2-z.txt", true,
"CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq,CpCqCrCsCtq,CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq",
4294967295, 18446744073709551614, true, false,
"CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq", true, 18446744073709551615, 134217728,
false, null, true).
0.15 ms taken to obtain 66 helper proof candidates, i.e. the minimal set of
referenced proofs such that each proof contains only a single rule with inputs.
20.83 ms taken to morph and parse 84 abstract proofs.
0.04 ms taken to validate 18 conclusions.
0.03 ms taken to find 5 occurrences of 5 theorems.
There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 11).
There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
There are 417 steps towards CCNppp / CCN0.0.0 (index 15).
There are 1877 steps towards CCNpNqCqp / CCN0N1C1.0 (index 17).
0.01 ms taken to count 2439 relevant proof steps in total.
0.03 ms taken to obtain 84 referenced indices.
0.03 ms taken to obtain 8 dedicated indices.
0.05 ms taken to build transformed proof.
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CpCCNqCCNCCNrCCNstNCNpuCsrvNCwwq =
DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
[6] CCNppp =
DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11[5]
[7] CCNpNqCqp = DDD1D[3][6]DDD1DDD1DDD1D[3][6]DDD1[6]1[5][5][1]11[5][5]
0.05 ms taken to print 585 bytes.
Wed Jul 10 18:29:08 2024: Process terminated. [pid: 23984, tid:1]
You may add a short remark about this in your solution (in comment) or under
your solution (as reply), then I will credit you for this as well.
________________________________
Von: Discher, Samiro
Gesendet: Mittwoch, 10. Juli 2024 18:46:16
An: [email protected]
Betreff: AW: [Metamath] Re: Shortest possible axiom for propositional calculus
> I managed to prove ax3 from w2 manually!
Indeed, nice.
Compactly written, that is
CpCCqCprCCNrCCNstqCsr = 1
[0] CpCCNqCCNrsCNqCCNCCNtCCNuvNpCutwNCxCCyCxzCCNzCCNabyCazCrq = DDDDD111111
[1] Cpp = DDD11DDD11D11[0][0]
[2] CpCqCrCsCtq = DDDDD1DDD11DD1D111[0]1[0]11
[3] CpCqp = DDD1D[2]1D111
[4] CpCNpq = DDDDD1D111[0]DDD11DDD1D111[0][0]1
[5] CCNppp =
DDDDD1[1]1DDDD11DDD1DDD11DD11DDD1D111[0][2]D11DDD11DDD1D111[0]1DDD1DDDD11D1DD1DDD1[0]D1111[0]DDD11D1[0][0]DDD1D1D[2]11[0][0]11DDDDD1D111[0]DDD11DDD1D111[0][0]DDD11DDD1111DDD11DDD1DDD1DDD11D11[0]111[0]1
[6] CpCCNqqq = D[3][5]
[7] CCNpNqCqp = DDD1[6]DDD1DDD1DDD1[6]DDD1[5]1[6][6][1]11[6][6]
and
./pmGenerator --transform data/w2.txt -f -n -t
CpCqp,CCNpNqCqp,Cpp,CCNppp,CpCNpq -p -2 -d
now prints
There are 35 steps towards Cpp / C0.0 (index 8).
There are 53 steps towards CpCqp / C0C1.0 (index 11).
There are 57 steps towards CpCNpq / C0CN0.1 (index 13).
There are 417 steps towards CCNppp / CCN0.0.0 (index 14).
There are 3301 steps towards CCNpNqCqp / CCN0N1C1.0 (index 16).
i.e. this is a "w2: A3: ω↦3301" improvement, the biggest so far 😃.
Congratulations!
Could you also post your solution and procedure/details at
https://github.com/xamidi/pmGenerator/discussions/2?
________________________________
Von: [email protected] <[email protected]> im Auftrag von
Steven Nguyen <[email protected]>
Gesendet: Mittwoch, 10. Juli 2024 18:24:46
An: [email protected]
Betreff: Re: [Metamath] Re: Shortest possible axiom for propositional calculus
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]<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com<https://groups.google.com/d/msgid/metamath/CAAfCLnhtUBBz7i9V0QMj8NJidzOMrhUTa4CLe7%2BSS9FynSGMwA%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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/604f022cd0d74bf2836da143d753be96%40rwth-aachen.de.
