Skip to content

refactor(NumberTheory): golf Mathlib/NumberTheory/PythagoreanTriples#38454

Open
yuanyi-350 wants to merge 2 commits intoleanprover-community:masterfrom
yuanyi-350:N_8
Open

refactor(NumberTheory): golf Mathlib/NumberTheory/PythagoreanTriples#38454
yuanyi-350 wants to merge 2 commits intoleanprover-community:masterfrom
yuanyi-350:N_8

Conversation

@yuanyi-350
Copy link
Copy Markdown
Collaborator

  • simplifies the Int.gcd x y = 0 branches in gcd_dvd, normalize, and classified using Int.gcd_eq_zero_iff
  • shortens the zero case in normalize to a direct simpa from PythagoreanTriple.zero

Extracted from #38144

Open in Gitpod

@yuanyi-350 yuanyi-350 added codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly labels Apr 24, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented Apr 24, 2026

PR summary e18244a4f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

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

@github-actions github-actions Bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label Apr 24, 2026
@yuanyi-350
Copy link
Copy Markdown
Collaborator Author

I ran a profiler comparison for the changed declarations in this PR.

Results (seconds):

  • PythagoreanTriple.gcd_dvd: 0.113373 -> 0.124069 (+9.43%)
  • PythagoreanTriple.normalize: 0.109086 -> 0.217934 (+99.79%)
  • PythagoreanTriple.classified: 0.025653 -> 0.022601 (-11.90%)

Overall:

  • classified is a bit faster
  • gcd_dvd regresses slightly
  • normalize regresses substantially and dominates the overall change

@yuanyi-350
Copy link
Copy Markdown
Collaborator Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 24, 2026

Benchmark results for dcb553d against e18244a are in. No significant results found. @yuanyi-350

  • build//instructions: -11.2G (-0.01%)

No significant changes detected.

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

maintainer merge

@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by MichaelStollBayreuth.

@mathlib-triage mathlib-triage Bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 25, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

codex OpenAI Codex wrote (parts of) this PR. LLM-generated PRs with substantial input from LLMs - review accordingly maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants