Groups keyboard shortcuts have been updated
Dismiss
See shortcuts

Upcoming contributions to proof minimization challenges

200 views
Skip to first unread message

samiro.d...@rwth-aachen.de

unread,
Jan 6, 2025, 6:44:29 AMJan 6
to Metamath
In probably at most a few weeks, I will post some weighty proof minimizations.
I don't know if anyone else is currently working on those, but in this case I would suggest to hurry up. :-)


I am throwing a lot of computing power at a new proof compression algorithm that I will release as part of pmGenerator along with these contributions.

Afterwards, it will be extremely difficult to make further non-tiny contributions (unless I missed something significant).


— Samiro Discher

Gino Giotto

unread,
Jan 8, 2025, 4:40:28 PMJan 8
to Metamath
I might have something. I created a Metamath database for Walsh's fourth axiom https://github.com/GinoGiotto/w4.mm and my proof for luk1 seems shorter than the current one.

Preliminary information:

- All theorems are complete and verified with metamath.exe.

- I saved all proofs in the normal format because the compressed one shows a lower step count (yes, this makes the database very big).

- The command "SHOW TRACE_BACK luk1 /COUNT /ESSENTIAL" says that "The proof would have 9513 steps if fully expanded back to
axiom references." which is lower than the 11989 step count in the table.

So, if the metamath.exe count is correct and if I have not made rookie mistakes then I have a shortening of luk1 in w4. I am not 100% confident that everything is fine until I translate it into condensed detachment and verify it with pmGenerator.

This email is just to claim my (potential) result before the new proofs arrive. I'm probably going to do the translation tomorrow or the day after tomorrow, and I will also attempt to shorten the proof further with the automatic compression algorithm. Hopefully everything is right. Fingers crossed.

Discher, Samiro

unread,
Jan 9, 2025, 12:14:09 AMJan 9
to Metamath
> Hopefully everything is right. Fingers crossed.

So it seems! As far as I can see, it reduces to 2437 steps towards L1 using --transform -z, but I only used the five theorems from w4.mm (which are ax1, id, luk1, luk2, th0), not the inferences — but you could still use their greatest subproofs of theorems as well. I attached my translation of your entire w4.mm to this mail (with inferences commented out).

$ ./pmGenerator -c -n -s CpCCNqCCNrsCtqCCrtCrq --parse data/w4-dProofs-GG.txt -f -n -s -d -o data/tmp.txt --transform data/tmp.txt -f -n -t CCNpCCNqrCspCCqsCqp,CpCqp,Cpp,CCNppp,CCpqCCqrCpr -p -2 -d
> There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 (index 0).
> There are 59 steps towards CpCqp / C0C1.0 (index 13).
> There are 465 steps towards Cpp / C0.0 (index 21).
> There are 1703 steps towards CCNppp / CCN0.0.0 (index 22).
> There are 9513 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23).
Using -z in the end resulted in:
> There are 3 steps towards CCNpCCNqrCspCCqsCqp / CCN0CCN1.2C3.0CC1.3C1.0 (index 0).
> There are 59 steps towards CpCqp / C0C1.0 (index 13).
> There are 465 steps towards Cpp / C0.0 (index 21).
> There are 1703 steps towards CCNppp / CCN0.0.0 (index 22).
> There are 2437 steps towards CCpqCCqrCpr / CC0.1CC1.2C0.2 (index 23).

Spoiler: My incoming w4:L1 will still be multiple times smaller (currently 827, unphased by compressing with your proofs of theorems :-), and even w4:id went down to 361 steps.


Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Gino Giotto <ginogiott...@gmail.com>
Gesendet: Mittwoch, 8. Januar 2025 22:40
An: Metamath
Betreff: [Metamath] Re: Upcoming contributions to proof minimization challenges
 
--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/a327629a-f1e2-4437-a6d9-50ae7095235an%40googlegroups.com.
w4-dProofs-GG.txt

samiro.d...@rwth-aachen.de

unread,
Jan 9, 2025, 6:32:19 AMJan 9
to Metamath
Another remark, when starting from all challenge proofs from w4, i.e. by adding the result of
./pmGenerator --unfold data/w4.txt -f -n -t CpCqp,CCpCqrCCpqCpr,CCNpNqCqp,Cpp,CCpqCCqrCpr,CCNppp,CpCNpq -o data/tmp2.txt -d
to w4-dProofs-GG.txt before proof compression, there are further reductions w4: (A2: 13819↦4215, L1: 11989↦2385).

Gino Giotto

unread,
Jan 10, 2025, 2:31:53 PMJan 10
to Metamath
For those who may be interested, the proposed shortenings have now been applied, along with an explanation of how I manually derived the one for L1 https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-11797219.

Discher, Samiro

unread,
Jan 26, 2025, 11:40:21 AMJan 26
to Metamath


And it will apparently stay #1 a little longer — post-processing my results with many theorems is taking several weeks longer (and is more productive) than I expected.

Gesendet: Freitag, 10. Januar 2025 20:31:53
An: Metamath
Betreff: Re: [Metamath] Re: Upcoming contributions to proof minimization challenges
 
For those who may be interested, the proposed shortenings have now been applied, along with an explanation of how I manually derived the one for L1 https://github.com/xamidi/pmGenerator/discussions/2#discussioncomment-11797219.

--
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 metamath+u...@googlegroups.com.
Reply all
Reply to author
Forward
0 new messages