feat(NumberTheory): add unitary divisors and unitary perfect numbers by chainstart · Pull Request #33838 · leanprover-community/mathlib4

chainstart · 2026-01-11T06:53:38Z

Summary

This PR introduces the unitary divisor sum function σ* to Mathlib and proves that no odd unitary perfect numbers exist.

Main Definitions

Nat.UnitaryDivisor d n: A divisor d of n is unitary if gcd(d, n/d) = 1
Nat.unitaryDivisors n: The Finset of all unitary divisors of n
Nat.unitaryDivisorSum n (notation σ*): Sum of all unitary divisors
Nat.UnitaryPerfect n: n is unitary perfect if σ*(n) = 2n

Main Theorems

Multiplicativity:

unitaryDivisorSum_mul: For coprime m, n, σ*(mn) = σ*(m) · σ*(n)
- Proved via explicit bijection between unitary divisors of mn and pairs of unitary divisors

Prime Powers:

unitaryDivisors_prime_pow: The unitary divisors of p^k are exactly {1, p^k}
unitaryDivisorSum_prime_pow: For prime p and k ≥ 1, σ*(p^k) = p^k + 1

Unitary Perfect Numbers:

no_odd_unitary_perfect: There are no odd unitary perfect numbers > 1 (Subbarao-Warren 1966)
UnitaryPerfect.even: Every unitary perfect number is even
UnitaryPerfect.eq_two_pow_mul_odd: Every unitary perfect number has form 2^a · k with a ≥ 1, k odd

Mathematical Background

A unitary perfect number is a positive integer n such that the sum of its unitary divisors equals 2n. This generalizes the classical perfect numbers. Only five unitary perfect numbers are known: 6, 60, 90, 87360, and one with 24 digits.

The main theorem (no odd unitary perfect numbers) was originally proved by Subbarao & Warren (1966) using prime factorization arguments. Our formalization uses Nat.recOnPrimeCoprime for structural induction.

References

Subbarao, M. V., & Warren, L. J. (1966). Unitary perfect numbers. Canadian Mathematical Bulletin, 9(2), 147-153.
Wall, C. R. (1975). The fifth unitary perfect number. Canadian Mathematical Bulletin, 18(1), 115-122.

Code Statistics

Files: 2
Lines: ~520
Theorems: 21 public declarations
Sorry count: 0

Checklist

All theorem names follow mathlib conventions
All lines ≤ 100 characters
All public theorems have docstrings
No sorry or admit
Code builds successfully
CI tests pass (awaiting verification)

This PR adds the unitary divisor sum function σ* and proves that no odd unitary perfect numbers exist. **Main definitions:** - `Nat.UnitaryDivisor`: A divisor d of n is unitary if gcd(d, n/d) = 1 - `Nat.unitaryDivisors`: The finset of unitary divisors - `Nat.unitaryDivisorSum`: The sum σ*(n) of unitary divisors - `Nat.UnitaryPerfect`: A number n is unitary perfect if σ*(n) = 2n **Main theorems:** - `unitaryDivisorSum_mul`: Multiplicativity of σ* for coprime arguments - `unitaryDivisorSum_prime_pow`: For prime p, σ*(p^k) = p^k + 1 - `no_odd_unitary_perfect`: No odd unitary perfect numbers exist (Subbarao-Warren 1966) - `UnitaryPerfect.even`: Every unitary perfect number is even The proofs use explicit bijection constructions for multiplicativity and structural induction on prime factorizations for the main theorem. References: - Subbarao & Warren (1966), Canadian Mathematical Bulletin 9(2), 147-153 - Wall (1975), Canadian Mathematical Bulletin 18(1), 115-122

github-actions · 2026-01-11T06:55:02Z

PR summary 76f94b4301

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.NumberTheory.UnitaryDivisor` (new file)	895
`Mathlib.NumberTheory.UnitaryPerfect` (new file)	896

Declarations diff

+ UnitaryDivisor
+ UnitaryPerfect
+ UnitaryPerfect.eq_two_pow_mul_odd
+ UnitaryPerfect.even
+ four_not_dvd_two_mul_odd
+ isMultiplicative_unitaryDivisorSum
+ mem_unitaryDivisors
+ no_odd_unitary_perfect
+ one_mem_unitaryDivisors
+ self_mem_unitaryDivisors
+ unitaryDivisorSum
+ unitaryDivisorSum_apply
+ unitaryDivisorSum_coprime_four_dvd
+ unitaryDivisorSum_mul
+ unitaryDivisorSum_odd_even
+ unitaryDivisorSum_odd_prime_pow_even
+ unitaryDivisorSum_one
+ unitaryDivisorSum_prime_pow
+ unitaryDivisor_mul_of_coprime
+ unitaryDivisor_one
+ unitaryDivisor_self
+ unitaryDivisors
+ unitaryDivisors_prime_pow

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

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

- Replace show with change (linter requirement) - Fix recOnPrimeCoprime branch names (h0/hp/h → zero/prime_pow/coprime) - Replace ring with ac_rfl (no Tactic import) - Replace interval_cases with omega - Fix simp+omega patterns for proper proof completion - Simplify calc chain for 4-divisibility proof

- Add 'module' keyword after copyright - Use 'public import' instead of 'import' - Add '@[expose] public section' before namespace - This follows mathlib4 module system requirements

SnirBroshi · 2026-01-11T13:37:04Z

+  (Nat.divisors n).filter fun d => Nat.gcd d (n / d) = 1
+
+/-- The unitary divisor sum function `σ*(n)`, equal to the sum of all unitary divisors. -/
+def unitaryDivisorSum (n : ℕ) : ℕ :=


Can you define it as an ArithmeticFunction?

Done. I've redefined unitaryDivisorSum as an ArithmeticFunction ℕ (see line 74). The notation is now scoped under ArithmeticFunction.UnitaryDivisorSum.

SnirBroshi · 2026-01-11T13:37:53Z

+This is proved by establishing a bijection between unitary divisors of `m*n` and
+pairs `(d₁, d₂)` of unitary divisors of `m` and `n` respectively. The bijection is
+`d ↦ (gcd(d,m), gcd(d,n))` with inverse `(d₁, d₂) ↦ d₁ * d₂`. -/
+theorem unitaryDivisorSum_mul {m n : ℕ} (hcoprime : Nat.Coprime m n) (hm : m ≠ 0) (hn : n ≠ 0) :


Can you prove ArithmeticFunction.IsMultiplicative?

Done. Added isMultiplicative_unitaryDivisorSum theorem (see line 354) with the @[arith_mult] attribute. Thank you for the suggestions!

Address PR review feedback: - Redefine unitaryDivisorSum as ArithmeticFunction instead of plain function - Add isMultiplicative_unitaryDivisorSum theorem proving multiplicativity - Add ArithmeticFunction.Defs import - Update notation to use scoped namespace - Remove unnecessary Mathlib.Tactic import

Fix CI build error by restoring: - `module` keyword after copyright header - `public import` instead of plain `import` These are required by mathlib4's module system.

tb65536 · 2026-01-16T08:56:59Z

+
+This file defines unitary divisors and the unitary divisor sum function σ*.
+
+A divisor `d` of `n` is called a *unitary divisor* if `gcd(d, n/d) = 1`. The unitary


Just noting that in group theory these are called Hall divisors.

Thanks for the suggestion! Added a note mentioning Hall divisors.

riccardobrasca · 2026-01-16T09:28:54Z

Dear @chainstart,
first of all thanks for your contribution! Can you provide a little mathematical motivation behind these notions? I am asking because this seems a little niche to me (but I may be wrong!) and maybe more suitable for another repository than for mathlib. Especially the notion of unitary perfect number seems unlikely to be used by someone else.

Ruben-VandeVelde · 2026-01-17T08:52:27Z

+      exact absurd ⟨hn0, hsum⟩ (no_odd_unitary_perfect hodd hgt1)
+
+/-- Every unitary perfect number can be written as `2^a * k` where `a ≥ 1` and `k` is odd. -/
+theorem UnitaryPerfect.eq_two_pow_mul_odd {n : ℕ} (h : UnitaryPerfect n) :


This is a property of any nonzero even natural number, so I'd suggest adding the following next to Nat.exists_eq_two_pow_mul_odd:

theorem Nat.eq_two_pow_mul_odd_of_even {n : ℕ} (h : Even n) (hn0 : n ≠ 0): ∃ a k : ℕ, a ≠ 0 ∧ Odd k ∧ n = 2 ^ a * k := by obtain ⟨a, k, hk_odd, hdecomp⟩ := Nat.exists_eq_two_pow_mul_odd hn0 refine ⟨a, k, ?_, hk_odd, hdecomp⟩ rintro rfl rw [hdecomp, pow_zero, one_mul, ← Nat.not_odd_iff_even] at h contradiction

Good point - this is indeed a general property of even numbers. I'll leave this for a separate PR to the core Nat files, as it would be more appropriate there.

Ruben-VandeVelde · 2026-01-17T08:53:05Z

+
+namespace Nat
+
+open BigOperators


Don't think you need this anymore

Removed, thanks!

Ruben-VandeVelde · 2026-01-17T08:54:00Z

+
+namespace Nat
+
+open BigOperators Finset


Suggested change

open BigOperators Finset

open Finset

Done, thanks!

Ruben-VandeVelde · 2026-01-17T08:57:57Z

+    by_cases hn_eq_1 : n = 1
+    · rw [hn_eq_1, unitaryDivisorSum_one] at hsum
+      omega
+    · have hgt1 : n > 1 := by
+        rcases n with _ | n'
+        · exact absurd rfl hn0
+        · rcases n' with _ | _
+          · exact absurd rfl hn_eq_1
+          · omega
+      exact absurd ⟨hn0, hsum⟩ (no_odd_unitary_perfect hodd hgt1)


Could be

Suggested change

by_cases hn_eq_1 : n = 1

· rw [hn_eq_1, unitaryDivisorSum_one] at hsum

omega

· have hgt1 : n > 1 := by

rcases n with _ | n'

· exact absurd rfl hn0

· rcases n' with _ | _

· exact absurd rfl hn_eq_1

· omega

exact absurd ⟨hn0, hsum⟩ (no_odd_unitary_perfect hodd hgt1)

cases (one_le_iff_ne_zero.mpr hn0).eq_or_lt' with

| inl hn_eq_1 =>

rw [hn_eq_1, unitaryDivisorSum_one] at hsum

omega

| inr hgt1 =>

exact absurd ⟨hn0, hsum⟩ (no_odd_unitary_perfect hodd hgt1)

Applied, thanks!

Changes: - Add Hall divisors terminology note (tb65536) - Simplify open statements: use `open Finset` (Ruben-VandeVelde) - Remove unused `open BigOperators` (Ruben-VandeVelde) - Simplify UnitaryPerfect.even proof with cases syntax (Ruben-VandeVelde) - Add structure_divides_odd_part theorem: if m = 2^a × M is UPN, then (1 + 2^a) | M - Remove redundant theorems (unitaryDivisorSum_ge_self, unitaryDivisorSum_ge_succ, eq_two_pow_mul_odd)

- Add Hall divisors terminology note (tb65536) - Simplify open statements: remove BigOperators (Ruben-VandeVelde) - Simplify UnitaryPerfect.even proof with cases syntax (Ruben-VandeVelde)

chainstart · 2026-01-17T14:00:39Z

Dear @riccardobrasca,

Thank you for the question! Let me explain the motivation:

I am currently working on Erdős Problem 1052, which asks whether there are only finitely many unitary perfect numbers. During this work, I found that Mathlib lacks the basic infrastructure for unitary divisors and the unitary divisor sum function σ*. So I developed these definitions and theorems both for my own proofs and for others working in this area.

As I make further progress on the UPN problem, I plan to contribute more results to Mathlib. At that point, you can reassess our PR and whether it is worth merging into Mathlib. Thanks!

riccardobrasca · 2026-02-13T13:42:33Z

Dear @chainstart I am inclined to to close this PR because unitary perfect numbers is a too specialized subject. I understand they appear in an Erdos problem, but as you know there are literally hundreds of them, and we simply don't have the energy to maintain a library of all such problems. What about submitting this to the formal conjecture repository?

robin-carlier · 2026-02-17T15:15:56Z

Hi @chainstart,

Thanks for the PR. After a small discussion within reviewers, we agree with @riccardobrasca that we might not want this within Mathlib for now, as there are too many side definitions in Erdös problems, and that this might be material more fit for the formal conjecture repository.

This might feel like a bit of a disappointment to you after the time invested in this PR, but please do not feel discouraged to open more PRs to Mathlib!

github-actions Bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize) labels Jan 11, 2026

chainstart added 4 commits January 11, 2026 15:14

fix: resolve CI errors - remove Tactic import, fix API usage

fd36ce0

fix: replace ring with ac_rfl for commutativity

60d2318

fix: add module declaration and expose section

e27131d

- Add 'module' keyword after copyright - Use 'public import' instead of 'import' - Add '@[expose] public section' before namespace - This follows mathlib4 module system requirements

SnirBroshi reviewed Jan 11, 2026

View reviewed changes

chainstart added 3 commits January 12, 2026 21:11

fix: use Finset.notMem_singleton

f38d684

fix: restore module declaration and public imports

ea3cf88

Fix CI build error by restoring: - `module` keyword after copyright header - `public import` instead of plain `import` These are required by mathlib4's module system.

leanprover-community-bot-assistant assigned riccardobrasca Jan 16, 2026

tb65536 reviewed Jan 16, 2026

View reviewed changes

Ruben-VandeVelde reviewed Jan 17, 2026

View reviewed changes

chainstart changed the title ~~feat(NumberTheory): add unitary divisor sum function~~ feat(NumberTheory): add unitary divisors and unitary perfect numbers Jan 17, 2026

chainstart added 3 commits January 17, 2026 19:52

fix: remove import Mathlib.Tactic and use change instead of show

cbb5b8e

Address reviewer feedback

ea00c06

- Add Hall divisors terminology note (tb65536) - Simplify open statements: remove BigOperators (Ruben-VandeVelde) - Simplify UnitaryPerfect.even proof with cases syntax (Ruben-VandeVelde)

robin-carlier closed this Feb 17, 2026


		This file defines unitary divisors and the unitary divisor sum function σ*.

		A divisor `d` of `n` is called a unitary divisor if `gcd(d, n/d) = 1`. The unitary

Conversation

chainstart commented Jan 11, 2026

Summary

Main Definitions

Main Theorems

Mathematical Background

References

Code Statistics

Checklist

Uh oh!

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

Uh oh!

PR summary 76f94b4301

Import changes for modified files

Declarations diff

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

riccardobrasca commented Jan 16, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chainstart commented Jan 17, 2026

Uh oh!

riccardobrasca commented Feb 13, 2026

Uh oh!

robin-carlier commented Feb 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions Bot commented Jan 11, 2026 •

edited

Loading

riccardobrasca commented Jan 16, 2026 •

edited

Loading