refactor(NumberTheory): Golf 100 files#38144
Open
yuanyi-350 wants to merge 11 commits intoleanprover-community:masterfrom
Open
refactor(NumberTheory): Golf 100 files#38144yuanyi-350 wants to merge 11 commits intoleanprover-community:masterfrom
yuanyi-350 wants to merge 11 commits intoleanprover-community:masterfrom
Conversation
This reverts commit 5a25d45.
github-actions
bot
added
the
large-import
PR summary 71f5543cfdImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.NumberTheory.FLT.Polynomial | 1405 | 1668 | +263 (+18.72%) |
| Mathlib.NumberTheory.Padics.PadicNorm | 931 | 934 | +3 (+0.32%) |
| Mathlib.NumberTheory.Padics.Hensel | 1744 | 1745 | +1 (+0.06%) |
Import changes for all files
| Files | Import difference |
|---|---|
15 filesMathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.AddChar Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Padics.ValuativeRel Mathlib.NumberTheory.Padics.WithVal Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.WittVector.Compare |
1 |
Mathlib.NumberTheory.Padics.PadicNorm |
3 |
Mathlib.NumberTheory.FLT.Polynomial |
263 |
Declarations diff
No declarations were harmed in the making of this PR! 🐙
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
bot
added
the
t-number-theory
yuanyi-350
added
codex
grunweg
added
the
awaiting-CI
github-actions
bot
removed
the
awaiting-CI
Contributor
|
These actually look pretty reasonable. Nice work! If you could split into smaller PRs, that would make reviewing easier and quicker (some of these are clearer improvements than others, and some will require more specialized reviewing knowledge to make sure that the new proofs are using the API in a healthy maintainable way). Also, you should change the title of the PR to avoid scaring off reviewers :) |
This was referenced Apr 18, 2026
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
mathlib-bors bot
pushed a commit
that referenced
this pull request
Apr 19, 2026
This PR selectively ports part of #38144 and only migrates the changes in: - `Mathlib/NumberTheory/FactorisationProperties.lean` Concretely, this PR: - rewrites `Prime.not_pseudoperfect` to use `Prime.properDivisors` and `Finset.sum_le_sum_of_subset` directly, instead of analyzing the powerset of proper divisors by cases - shortens `Prime.not_perfect` to the direct consequence of `Prime.not_pseudoperfect` - refactors `Prime.deficient_pow` to reuse `properDivisors_prime_pow` and a simple mapped-sum identity, instead of reproving the structure of the proper divisors of a prime power inline
This was referenced Apr 20, 2026
mathlib-dependent-issues
bot
removed
the
blocked-by-other-PR
Contributor
|
Can you mark this PR as depend on the other smaller PRs (so that this PR doesn't show up on queue)? |
tb65536
added
the
awaiting-author
This was referenced Apr 20, 2026
yuanyi-350
removed
the
awaiting-author
Collaborator
Author
|
@tb65536 , done! |
mathlib-dependent-issues
bot
added
the
blocked-by-other-PR
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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.
This PR is an experimental project. In this PR, we use an Agent to automatically scan and attempt to simplify proofs. We hope to eventually effectively golf 100 files and avoid reinventing the wheel in mathlib.
We have chosen
Mathlib/NumberTheoryas the testing ground.If this experiment is very successful and accepted by the mathlib community, we would be honored to open source it.
The relevant projects includes
Mathlib/MeasureTheory.Mathlib/Analysis.This PR serves as an index. For the actual code review, please refer to the individual PRs linked below. Each of those PRs modifies only a single file to facilitate the review process.
FactorisationProperties#38204Mathlib/NumberTheory/NumberField/Norm#38277Mathlib/NumberTheory/ArithmeticFunction/Zeta#38278Mathlib/NumberTheory/NumberField/Basic#38279Mathlib/NumberTheory/Cyclotomic/Basic#38280