refactor(NumberTheory): Golf 100 files by yuanyi-350 · Pull Request #38144 · leanprover-community/mathlib4

yuanyi-350 · 2026-04-17T02:33:39Z

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/NumberTheory as 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

refactor(MeasureTheory): golf 100 files #38104, which golfs Mathlib/MeasureTheory.
refactor(Analysis): golf 100 files #37968, which golfs 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.

This reverts commit 5a25d45.

github-actions · 2026-04-17T02:34:40Z

PR summary 00427301b0

Import changes exceeding 2%

%	File
+18.71%	`Mathlib.NumberTheory.FLT.Polynomial`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.FLT.Polynomial	1406	1669	+263 (+18.71%)
Mathlib.NumberTheory.Padics.PadicNorm	931	934	+3 (+0.32%)
Mathlib.NumberTheory.Padics.Hensel	1745	1746	+1 (+0.06%)

Import changes for all files

Files	Import difference
15 files `Mathlib.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.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

tb65536 · 2026-04-18T09:30:09Z

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 :)

… into NT-golf

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

mathlib-dependent-issues · 2026-04-20T06:02:54Z

This PR/issue depends on:

… into NT-golf

tb65536 · 2026-04-20T08:58:12Z

Can you mark this PR as depend on the other smaller PRs (so that this PR doesn't show up on queue)?

yuanyi-350 · 2026-04-20T09:15:35Z

@tb65536 , done!

…38280) - refactors `Cyclotomic/Basic` by rewriting `nonempty_algEquiv_adjoin_of_isSepClosed` around `AlgHom.fieldRange_eq_map` and `IntermediateField.adjoin_map` - replaces the manual adjoin induction with direct `adjoin_le_iff` inclusions for the cyclotomic roots Extracted from #38144 , migrate from #38202 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

mathlib-merge-conflicts · 2026-04-21T22:32:36Z

This pull request has conflicts, please merge master and resolve them.

…38277) - refactors `NumberField/Norm` by moving `isUnit_norm_of_isGalois` after `dvd_norm` and shortening its proof to a direct application of `dvd_norm` together with `isUnit_of_dvd_unit` Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

…8351) - golfs `ADEInequality` by replacing repeated `inv_le_inv₀` proof blocks with direct applications of `inv_anti₀` - shortens `lt_three`, `lt_four`, and `lt_six` by removing the now-unneeded fixed-denominator positivity witnesses Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)

yuanyi-350 added 3 commits April 13, 2026 10:18

Merge branch 'golf_27'

5a25d45

Revert "Merge branch 'golf_27'"

0915ed3

This reverts commit 5a25d45.

golf

5611992

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Apr 17, 2026

github-actions Bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Apr 17, 2026

yuanyi-350 added codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly labels Apr 17, 2026

grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 17, 2026

fix ci

59a52e1

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 18, 2026

yuanyi-350 added 2 commits April 18, 2026 18:05

golf more files

a62fd7c

Merge branch 'NT-golf' of https://github.com/yuanyi-350/yuanyi_mathlib4…

f74837e

… into NT-golf

This was referenced Apr 18, 2026

refactor: golf only Cyclotomic/Basic, ArithmeticFunction/Zeta #38202

Closed

refactor: golf only Padics/Hensel, NumberField/Norm #38203

Closed

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 18, 2026

yuanyi-350 mentioned this pull request Apr 18, 2026

[Merged by Bors] - refactor: golf only FactorisationProperties #38204

Closed

Merge branch 'master' into NT-golf

6bc6be0

This was referenced Apr 20, 2026

refactor(Analysis): golf 100 files #37968

Open

refactor(MeasureTheory): golf 100 files #38104

Open

mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2026

yuanyi-350 added 4 commits April 20, 2026 15:35

Merge branch 'master' into NT-golf

8899d29

fix error

74f4b20

add more file

8384e97

Merge branch 'NT-golf' of https://github.com/yuanyi-350/yuanyi_mathlib4…

3e8e529

… into NT-golf

tb65536 added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 20, 2026

yuanyi-350 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 20, 2026

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 20, 2026

fix ci

1a3d336

mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 21, 2026

Merge branch 'master' into NT-golf

d07487a

github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 22, 2026

yuanyi-350 mentioned this pull request Apr 22, 2026

[Merged by Bors] - refactor(NumberTheory): golf Mathlib/NumberTheory/ADEInequality #38351

Closed

Merge branch 'master' into NT-golf

4828b37

This was referenced Apr 23, 2026

refactor(NumberTheory): golf Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas #38402

Open

refactor(NumberTheory): golf Mathlib/NumberTheory/LSeries/AbstractFuncEq #38403

Open

Merge branch 'master' into NT-golf

6eab1c6

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor(NumberTheory): Golf 100 files#38144

refactor(NumberTheory): Golf 100 files#38144
yuanyi-350 wants to merge 15 commits intoleanprover-community:masterfrom
yuanyi-350:NT-golf

yuanyi-350 commented Apr 17, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Apr 17, 2026 •

edited

Loading

Import changes for modified files

Uh oh!

tb65536 commented Apr 18, 2026

Uh oh!

mathlib-dependent-issues Bot commented Apr 20, 2026 •

edited

Loading

Uh oh!

tb65536 commented Apr 20, 2026

Uh oh!

yuanyi-350 commented Apr 20, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Apr 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

yuanyi-350 commented Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Apr 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 00427301b0

Import changes for modified files

Declarations diff

Uh oh!

tb65536 commented Apr 18, 2026

Uh oh!

mathlib-dependent-issues Bot commented Apr 20, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tb65536 commented Apr 20, 2026

Uh oh!

yuanyi-350 commented Apr 20, 2026

Uh oh!

mathlib-merge-conflicts Bot commented Apr 21, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

yuanyi-350 commented Apr 17, 2026 •

edited

Loading

github-actions Bot commented Apr 17, 2026 •

edited

Loading

mathlib-dependent-issues Bot commented Apr 20, 2026 •

edited

Loading