Shortened proofs 12 #3180
Merged
Shortened proofs 12 #3180
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
avekens
approved these changes
May 17, 2023
|
From time to time, I also run the minimization script, over the whole set.mm, but only for special minimization focussing on replacing certain theorems (not global ones like @GinoGiotto does). I never experienced problems with ~footex (maybe it was never affected). I had (runtime) problems with the ~fourier*, ~stirl* and ~stow* theorems, therefore I always exclude them. A good idea would be to shorten these (sometimes very long) proofs by extracting adequate lemmata... |
Merged
icecream17
added a commit
to icecream17/set.mm
that referenced
this pull request
Aug 24, 2024
I think minimizing flt4lem5e is prohibitively long because, despite only being 27 lines long, there are 71 Zs, so there are 46140 steps when expanded+syntax. (Relevant: metamath#3180) I used theorems in Scott's mathbox without even realizing, so they're moved now I renamed dvdspw to reduce confusion with dvdsexp Fix comment of ncoprmgcdne1bgd
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Continuation of #3127. Proof minimizer executed between the 11501th and the 12000th theorems that don't have a
proof modification is discouragedlabel in their comment.No new axiom dependencies are introduced. Scan my min-all branch and compare it to my develop branch for evidence. The result of the comparison should correspond to eb06148 + 4e9fa83.
Turns out I was optimistic about the amount of time it would take for my computer to finish the job, but it's finally done. I updated the min-all branch up to the final commit (which is min25.5). A few more theorems had their axiom usage reduced, so I updated the file listing axiom usage too (already linked above). I think this is good evidence that the minimizer is reliable, as none of the 25,475 analyzed theorems exhibited a single occurrence of accidental axiom additions.
Minimizing proofs in a systematic way takes a really long time, requiring weeks of computing power active 24/7, even during the night. I think we would benefit greatly if PR metamath/metamath-exe#94 would be merged soon, as it claims to halve the time required to do these minimizations. I encourage the community to direct its attention towards it, it already has one approval and from reading comments it doesn't seems there are reasons to keep it pending further @digama0.
I have no idea how Norm used to do this flawlessly. The minimizer is incredibly fast for the first thousands theorems and then becomes exponentially slower towards the end of main. Theorem
footexliterally crashed metamath, so I wasn't even convinced to continue since there could have been other ones that could have behaved the same way. I decided to give the minimizer a second chance, I skippedfootexand luckely no problems happened afterwards. Anyway I'll open an issue about that event.