Perfect Numbers

Stream: maths

[Aaron Anderson]

I have a rough but working proof of the Perfect Number/Euclid-Euler Theorem, Freek 70, at https://github.com/awainverse/perfect_number

[Aaron Anderson]

I’m interested in people’s input on several things. One thing that comes to mind is whether some of the nat variables should be replaced with pnats.

[Johan Commelin]

@Aaron Anderson Interesting! I will write some feedback after breakfast.

[Yury G. Kudryashov]

If it builds, then we can add it to our list.

[Yury G. Kudryashov]

Could you please open a PR to mathlib/archive? We'll probably want to merge some parts to src/ but it would be nice to have a green light from CI before adding a link to this PR to the website.

[Aaron Anderson]

I'm trying to figure out how, but creating my own repository to host this today was already stretching my understanding of github...

[Bryan Gin-ge Chen]

I just downloaded the repo and it built locally with no warnings or errors.

[Johan Commelin]

@Aaron Anderson We can coach you through it.

[Johan Commelin]

Are you on windows or linux?

[Johan Commelin]

(Or mac...)

[Aaron Anderson]

Linux.

[Johan Commelin]

Ooh great, than it's easy-peasy

[Johan Commelin]

You should have just received an email with an invitation for write access to mathlib.

[Aaron Anderson]

I know a few of the basic git commands at this point

[Johan Commelin]

Do you by chance have leanproject installed?

[Aaron Anderson]

Yes, and I used that to create my perfect_number repo

[Johan Commelin]

Ok, great.

[Aaron Anderson]

(I've accepted the email invitation)

[Johan Commelin]

@Aaron Anderson so if you accept that invitation, and then leanproject get mathlib (in a directory where you do not yet have a copy of mathlib), then you are halfway there.

[Aaron Anderson]

Ok, I've done that, and have a "mathlib" folder on my computer.

[Johan Commelin]

After that, you can write

git checkout -b freek-70

[Johan Commelin]

This creates a new branch, for your PR

[Johan Commelin]

After that, you have to copy your file to
archive/100-theorems-list/70_perfect_numbers.lean

[Johan Commelin]

(Or something like that)

[Johan Commelin]

And then

git add archive/100-theorems-list/70_perfect_numbers.lean
git commit

[Johan Commelin]

In the commit message, you can use something like

feat(archive/100-theorems-list): perfect numbers (nr 70)

or something better (-;

[Johan Commelin]

Once you have done that:

git push

and this will give an error message, saying that you need to set an upstream thingy. It will tell you which command to execute instead. Do that.

[Johan Commelin]

This last command will give you a URL in it's output. You can visit that URL to open a PR.
(Alternatively, just go to the mathlib page on github, and it will recognise that you recently pushed a branch, and suggest to open a PR.)

[Johan Commelin]

Finally, you can (if you want :stuck_out_tongue_wink:) post a message here of the form #3057 where 3057 is the PR number on the github page, and Zulip will automatically turn it into a link that we can click on to see your latest creation.

[Johan Commelin]

Now for some feedback on the code. I've gone through the first 100 lines or so.

import data.nat.totient

open_locale classical
open_locale big_operators

section definitions

variable (n : ℕ)

def divisors : finset ℕ :=
finset.filter (λ x : ℕ, x ∣ n) (finset.Ico 1 (n + 1))

def proper_divisors : finset ℕ :=
finset.filter (λ x : ℕ, x ∣ n) (finset.Ico 1 n)

lemma not_proper_self :
  n ∉ proper_divisors n :=
by simp [proper_divisors]

lemma mem_divisors {m : ℕ} :
n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0:=
begin
  suffices : n ∣ m ∧ 1 ≤ n ∧ n < m + 1 ↔ n ∣ m ∧ ¬m = 0,
  by simpa only [divisors, finset.Ico.mem, ne.def, finset.mem_filter, and_comm],
  split,
  { intro hyp, refine ⟨hyp.left, _⟩, have h1 := hyp.right, omega },
  { intro hyp, refine ⟨hyp.left, _⟩,
    rcases hyp with ⟨⟨c, rfl⟩, nonzero⟩,
    split,
    { cases n,
      { simpa using nonzero },
      { exact nat.le_add_left _ _, }, },
    { cases c,
      { simpa using nonzero },
      { calc n = n * 1           : by rw mul_one
           ... ≤ n * (c + 1)     : nat.mul_le_mul_left _ (nat.le_add_left _ _)
           ... < n * (c + 1) + 1 : nat.lt_succ_self _, } } }
end

variable {n}

lemma le_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ≤ m :=
by { rw [mem_divisors, ← nat.pos_iff_ne_zero] at h, apply nat.le_of_dvd h.2 h.1 }

variable (n)

--lemma mem_proper_divisors : sorry := sorry

lemma divisors_eq_proper_divisors_insert_self (posn : 0 < n) :
  divisors n = insert n (proper_divisors n) :=
begin
  ext,
  simp only [finset.mem_insert, divisors, proper_divisors, finset.Ico.succ_top posn,
    finset.filter_insert, if_true, dvd_refl, finset.mem_insert],
end

def sum_divisors : ℕ :=
∑ i in divisors n, i

def sum_proper_divisors : ℕ :=
∑ i in proper_divisors n, i

@[simp] lemma divisors_zero : divisors 0 = ∅ := dec_trivial

@[simp] lemma proper_divisors_zero : proper_divisors 0 = ∅ := dec_trivial

@[simp] lemma sum_divisors_zero : sum_divisors 0 = 0 := dec_trivial

@[simp] lemma sum_proper_divisors_zero : sum_proper_divisors 0 = 0 := dec_trivial

lemma sum_divisors_eq_sum_proper_divisors_add_self :
sum_divisors n = sum_proper_divisors n + n :=
begin
  by_cases h : n = 0, { simp [h] },
  replace h : 0 < n := nat.pos_iff_ne_zero.mpr h,
  rw [sum_divisors, sum_proper_divisors, divisors_eq_proper_divisors_insert_self _ h,
    finset.sum_insert (not_proper_self _), add_comm],
end

def perfect : Prop :=
sum_proper_divisors n = n

end definitions

section basic_lemmas

lemma perfect_iff_sum_divisors_twice {n : ℕ} :
  perfect n ↔ sum_divisors n = 2 * n :=
by { rw [sum_divisors_eq_sum_proper_divisors_add_self, perfect], omega }

@[simp] lemma divisors_one : divisors 1 = ({1} : finset ℕ) :=
by { ext, rw mem_divisors, simp }

lemma one_mem_divisors {n : ℕ} (nonzero : n ≠ 0):
1 ∈ divisors n :=
by simp [mem_divisors, nonzero]

lemma self_mem_divisors {n : ℕ} (nonzero : n ≠ 0):
  n ∈ divisors n :=
by simp [mem_divisors, nonzero]

lemma pos_sum_divisors {n : ℕ} (posn : 0 < n) :
  0 < sum_divisors n :=
begin
  rw nat.pos_iff_ne_zero at posn,
  calc 0 = ∑ i in divisors n, 0 : finset.sum_const_zero.symm
     ... < sum_divisors n       : finset.sum_lt_sum (λ _ _, nat.zero_le _) _,
  use 1, exact ⟨one_mem_divisors posn, nat.zero_lt_one⟩,
end

[Aaron Anderson]

#3094

[Johan Commelin]

I should say that I think the code was already really good!

[Johan Commelin]

@Aaron Anderson Nice!

[Johan Commelin]

Another thing that can make your life easier: you often need to exclude n = 0. Sometimes you use 0 < n, sometimes 0 ≠ n. You should choose one, and use it everywhere. It will make it a lot easier to pass the assumption back and forth.
Now you constantly need to convert between the two versions.

[Aaron Anderson]

I'm still wondering if I do anything that'd make it difficult to just shift to pnats

[Johan Commelin]

It might help a bit... But I'm not sure if it will matter much

[Kevin Buzzard]

I think the correct thing to say here is "sure, just switch to pnats, and when you find holes in the pnat library just make a PR to mathlib which fixes them"

[Johan Commelin]

Another thing:

src/number_theory/lucas_lehmer.lean:def mersenne (p : ℕ) : ℕ := 2^p - 1

[Johan Commelin]

You could import that file.

[Johan Commelin]

Maybe it even contains some lemmas that you could reuse.

[Kevin Buzzard]

I think pnats deserve some more love

[Johan Commelin]

@Aaron Anderson and there is also

src/data/padics/padic_norm.lean:def padic_val_nat (p : ℕ) (n : ℕ) : ℕ :=

which can help with the multiplicity lemmas

[Johan Commelin]

@Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

[Johan Commelin]

@Aaron Anderson A lot of your lemmas seem useful and reusable. So we might want to butcher your file into tiny pieces that end up in 10 different places in mathlib.

[Aaron Anderson]

Awesome.

[Aaron Anderson]

I think pnats might be good for defining multiplicative functions in general

[Johan Commelin]

Feel free to experiment!

[Johan Commelin]

@Aaron Anderson By the way, probably relevant: if you want to make changes to the code in the PR, just edit the files in your clone of mathlib, and then git commit -a, write a message, and git push. That's it.

[Kenny Lau]

I use git commit -am "message"

[Patrick Massot]

Johan, if you don't have a convenient link you could have used instead of writing all those git explanations then you're welcome to copy paste this into our contributing guide, or a new file linked from our contributing guide.

[Yury G. Kudryashov]

Johan Commelin said:

Yury G. Kudryashov Don't you think that 95% of the code should go into src/?

I didn't look at the code yet.

[Aaron Anderson]

I've started refactoring to pnats. Proving inequalities is easier, but the tactics seem much weaker. Along the way, I found that having to switch between pnats and nats made me want to use nat.primes for my prime numbers, but this is maybe too cumbersome...

[Aaron Anderson]

It's in a new file here https://github.com/awainverse/perfect_number

[Aaron Anderson]

I'd like to be able to talk about multiplicative functions in general, and prove something to the effect of ∀ n : ℕ+, f(n) = (factorisation n).prod (λ p : nat.primes, λ k : ℕ, f (p ^ k)) for a multiplicative function f, and factorisation a finsupp of multiplicities

[Aaron Anderson]

I think this is a good argument that I should keep going on pnats, and maybe nat.primes?

[Kevin Buzzard]

The reason I would not use pnats if I were knocking off this sort of proof is precisely that they're not as well developed as nats, and the reason they're not as well developed is precisely because people don't use them. This vicious circle is not there for any particular reason and that's why I think keeping going on pnats is a good idea. Any factoring stuff will work better with pnats than nats the moment pnats have the right infrastructure. Pnats are a monoid with cancellation; monoids with 0 are a different thing somehow

[Aaron Anderson]

Well, I have no idea how the omega tactic works, other than sometimes it solves my problems with nats, but as I go I'm designating which lemmas about pnats maybe should be simp lemmas

[Aaron Anderson]

I'm proving (usually 2-line proofs or so) a lot of lemmas about pnats which are basically wrappers for existing nat lemmas. I think pnats would be way more useful if there was a common generalization of some kind of divisibility-structure, and facts about coprime and gcd were proved for that.

[Aaron Anderson]

I know that ring_theory/coprime exists, but pnats aren't a semiring, and gcd doesn't seem to be defined in that context.

[Aaron Anderson]

This probably wants some definition of a divisibilty poset?

[Aaron Anderson]

(Not at all necessary just to get this project in mathlib, but it'd be cool to start proving things about multiplicative functions, Dirichlet convolution, and even incidence algebras)

[Johan Commelin]

@Aaron Anderson Do you have any idea what kind of structure you need (weaker than semiring) in which you can prove your facts?

[Johan Commelin]

I guess (tongue in cheek) you might need a canonically_ordered_semirig

[Aaron Anderson]

I think that addition is unnecessary, a comm_monoid should be enough context

[Aaron Anderson]

Or perhaps has_dvd

[Bryan Gin-ge Chen]

Incidence algebras would be great!

[Aaron Anderson]

Something like “if you have an operation called gcd, which is provably equivalent to the sup in the poset with relation dvd, which has sensible properties, then you have these lemmas”

[Alex J. Best]

I did a tiny bit on incidence algebras a long time ago, its completely broken now :sad: (but I guess this means mathlib has advanced a lot) (and it was badly written / experimental to begin with) but just in case you are curious here is what I had:

import tactic
import data.rat.basic
import data.set.intervals
import data.set.finite
import init.algebra.order

open nat set

variable (α : Type*)

class locally_finite extends partial_order α :=
(fin_Icc : ∀ x y : α, fintype (Icc x y))

def my_Icc (n m : ℕ) : list ℕ := list.range' n (m - n + 1)
def Icc_multi (n m : ℕ) : multiset ℕ := my_Icc n m
theorem nodup (n m : ℕ) : list.nodup (my_Icc n m) :=
by dsimp [my_Icc]; simp [list.nodup_range']

theorem my_nodup (n m : ℕ) : multiset.nodup (Icc_multi n m) := nodup _ _
def tIcc (n m : ℕ) : finset ℕ := ⟨_, my_nodup n m⟩

instance Icc_ℕ_fintype (l u : ℕ) : fintype (Icc l u) :=
fintype.of_finset (tIcc l u) (λ x,
begin split, intro h,simp [h], split, {simp [(∈)] at h, sorry},sorry,sorry, end)

instance : partial_order ℕ := by apply_instance

instance : locally_finite ℕ :=
{ fin_Icc := λ x y, Icc_ℕ_fintype x y,
  ..nat.partial_order }

variables [locally_finite α] (R : Type*) [comm_ring R]

def incidence_algebra := α → α → R

def δ [decidable_eq α] : incidence_algebra α R :=
λ x y, if x = y then 1 else 0

#check δ ℕ ℤ
#eval δ ℕ ℤ 1 0

def ζ [@decidable_rel α (≤)] : incidence_algebra α R :=
λ x y, if x ≤ y then 1 else 0

#check ζ ℕ ℤ
#eval ζ ℕ ℤ 1 3
#eval ζ ℕ ℤ 1 0

instance [decidable_eq α] : has_one (incidence_algebra α R) := ⟨δ α R⟩

instance : has_mul (incidence_algebra α R) :=
⟨λ f g x y, finset.sum ((locally_finite.fin_Icc x y).elems) (λ z, f x z * g z y)⟩

#check (δ ℕ ℤ * δ ℕ ℤ)
#eval (δ ℕ ℤ * δ ℕ ℤ) 1 1
#eval (δ ℕ ℤ * ζ ℕ ℤ) 1 1

instance [decidable_eq α] : monoid (incidence_algebra α R) :=
{ mul := (*),
  mul_assoc := λ x y z, begin sorry end,
  one := (1),
  one_mul := λ a, begin ext x y, simp [(*),has_one.one,δ],sorry end,
  mul_one := sorry }

instance (x y : α) : fintype (Icc x y) := locally_finite.fin_Icc x y

lemma card_Icc_lt_card_Icc_of_lt (x y z : α) (hxz : x ≤ z) (hzy : z < y) : fintype.card (Icc x z) < fintype.card (Icc x y) :=
begin
   have hxy : x ≤ y := le_of_lt (lt_of_le_of_lt hxz hzy),
   have y_not_mem : y ∉ Icc x z := λ h, begin
      simp only [hxy, true_and, mem_Icc] at h,
      exact lt_irrefl _ (lt_of_le_of_lt h hzy),
   end,
   have y_mem : y ∈ Icc x y := by simp [hxy],
   have : Icc x z ⊆ Icc x y := Icc_subset_Icc_right (le_of_lt hzy),
   exact card_lt_card ⟨this, λ h, by cc⟩,
end

def μaux [decidable_eq α] (x : α) : α → R
| y := if x = y then 1 else begin
   haveI : fintype (Ico x y) := sorry,
   exact -finset.sum (fintype.elems (Ico x y)) (λ z,
      have fintype.card ↥(Icc x z) < fintype.card ↥(Icc x y) :=
         card_Icc_lt_card_Icc_of_lt α x y z.1 z.2.1 z.2.2,
      μaux z),
end
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ y,
   fintype.card (Icc x y)
)⟩]}

def μ [decidable_eq α] : incidence_algebra α R := λ x, μaux α R x

set_option pp.all false

example : μ ℕ ℤ = λ x y, if x = y then 1 else (if y = x + 1 then -1 else 0) :=
begin
   ext x y,
   split_ifs,
   {dsimp [μ], rwa [μaux, if_pos], },
   {dsimp [μ], rwa [μaux], rwa [if_neg, h_1], simp,
   have : Ico x (x + 1) = {x} := sorry,
   conv_lhs
   {
      rw [this],
      congr,
      skip,
      funext,
      rw [μaux],
      rw [if_pos (sorry  : x = ↑ z)],
   }, simp, have := (locally_finite.fin_Icc x (x+1)).complete, simp at this,
   norm_cast,
   rw finset.card_eq_one,
   use x,
   simp,
   dsimp,
   dunfold coe_sort,
   dunfold has_coe_to_sort.coe,dsimp,
   simp,
   ext,
   simp at a,
   split,
   intro h,

   have := this x (by simp),
   erw [(sorry : Icc x (x+1) = {x})] at this,  },
end
#eval μ ℕ ℤ 1 1
#check set.has_coe_to_sort
lemma (p) :  finset.sum (fintype.elems {x_1 : α // p x}) f

lemma μ_inv_ζ_eq_one [decidable_eq α] [@decidable_rel α (≤)] : μ α R * ζ α R = 1 := begin
ext x y,
dsimp,
simp [(*)],
unfold_coes,
   dunfold coe_sort,
   dunfold has_coe_to_sort.coe,dsimp,
   simp,
end


#lint

[Alex J. Best]

Looks like list.Icc still isn't in mathlib, maybe we should add this as a (help wanted / easy) issue on github rather than just a comment in https://github.com/leanprover-community/mathlib/blob/fbc9592788fe71b15bdefc972a98f40b79d29bab/src/data/list/intervals.lean#L19 so people can find it?

[Kevin Buzzard]

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

[Kevin Buzzard]

Note that nat isn't because of zero. But nat might well be a monoid with 0 with good factorisation properties. I was talking to @Chris Hughes about this the other day. The ideals in a commutative ring are a monoid and the ideals in a Dedekind domain are a monoid with a zero and, other than that, good factorisation properties. This all very much reminds me of @Johan Commelin 's group with 0 insight. There's some natural structure here that we're missing and we would like, but mathematicians didn't spot it yet. Is it an incidence algebra? I don't know what they are

[Bryan Gin-ge Chen]

Incidence algebras are what you define to generalize the Mobius inversion formula to settings like finite subsets where it becomes inclusion-exclusion.

[David Wärn]

Isn't nat a "canonically ordered comm monoid with lattice structure", where 0 is the maximal element? I think the problem with nat is that Dirichlet convolutions make no sense at 0, since a * b = 0 has infinitely many solutions

[Kevin Buzzard]

If the axioms work out for nat too then the situation is even better than I expected

[Kevin Buzzard]

The concept of a UFD generalises to monoids, was Chris' observation. And then there's this dichotomy depending on whether there's a 0 or not. At the end of the day the answer to the original question is that pnat as a monoid has the property that it is free, so you get all the juicy consequences of the universal property including a lattice structure with arbitrary nonzero infs. Does pnat have a lattice instance? Probably not because if there's an order it will be the usual one, not divisibility

[David Wärn]

I think there are at least three things happening with pnat that we can try to generalize:

• Dirichlet convolutions of arithmetic functions. Incidence algebras sort of make sense of this, but an element of the incidence algebra contains superfluous information. Another concept is this: given a ring R and a category C, such that every arrow in C has only finitely many factorisations into two arrows, we can form the "category algebra", which assigns a scalar in R to every arrow, and where convolution makes sense because of the finiteness condition. Given a monoid like pnat (but unlike nat under multiplication!) we can thus form the category algebra on the single object category, and get the usual notion of arithmetic function & Dirichlet convolution. We also get incidence algebras, since posets are categories. We get a "Zeta function" by assigning 1 to every arrow, and a "delta function" (identity for convolution) by assigning 1 to identity arrows and 0 to everything else.

• Multiplicative functions. Over "sufficiently nice" monoids (in particular free monoids like pnat), we can talk about multiplicative functions. I think for perfect numbers the relevant facts are "Zeta function is multiplicative", "the coercion pnat -> int is multiplicative", and "convolution of multiplicative functions is multiplicative".

• Möbius inversion.Sometimes we can find a Möbius function, inverse to the Zeta function. In particular it always exists in an incidence algebra.

[Kevin Buzzard]

It sounds like this incidence stuff is useful for the theory of so-called "multiplicative functions" (f(ab)=f(a)f(b) if gcd(a,b)=1), which do I think work on nat (f(0) can be anything). I wonder to what extent mobius inversion is useful though? I don't think you need it for perfect numbers

[Kevin Buzzard]

Note that the standard usage of the phrase in number theory books has this gcd condition -- a monoid hom is called a strictly multiplicative function in the number theory literature. Coefficients of certain modular forms are multiplicative but not monoid homs, somehow the weaker notion was isolated as being useful

[David Wärn]

Yes, multiplicative function is a good concept, but I'm not sure how it generalizes. Presumably there's a connection to be made with measures, which are only additive when your sets are disjoint

[David Wärn]

Meanwhile, the concept of category algebra generalizes matrix algebras (which I unsuccessfully tried to make sense of a while ago) as well, via indiscrete categories. What a concept!

[David Wärn]

I also don't think you need Möbius inversion for Perfect numbers -- but of course it's often useful for counting things. As far as I can see the main (only?) advantage of incidence algebras over category algebras is that you always have a Möbius function (the upshot of the category algebra is that you get the usual notion of arithmetic function).

[Aaron Anderson]

All you need right now for perfect numbers to work for pnats are some duplicate lemmas about gcd and stuff, which I’ve written, and an alteration of the fin_mult and coprime_part ideas to work with pnat.factors rather than multiplicity, which needs a semiring

[Aaron Anderson]

But I’m just thinking about how to avoid writing so many duplicate lemmas if I (or someone else) keeps writing related elementary number theory

[Aaron Anderson]

Kevin Buzzard said:

Isn't pnat a canonically ordered comm monoid with a lattice structure? Won't this be enough for most things?

This is likely what I'm looking for. There's no definition yet of a multiplicative canonically_ordered_comm_monoid, and maybe that's what I'm looking for... one problem I wouldn't know how to deal with is how to recognize dvd as a partial order, without interfering with the linear order le from the additive structure. Then also I'm not sure syntactically it'd be easy to prove things about the gcd function without just repeatedly rewriting gcd_eq_sup_dvd or something

[Yury G. Kudryashov]

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

[Aaron Anderson]

Yury G. Kudryashov said:

AFAIR there is some theory about "dvd as a partial order" in algebra/associated.

That does seem useful. I'd want to prove things about the special case where associates is a partial order, in bijection with the original monoid, because there's only one unit.

[Aaron Anderson]

I've retrofitted most of my file to deal with pnats, and created a new file, multiplicity_vectors.lean, that introduces yet another kind of prime factorisation (as a finsupp), but contains a lot of sorries

[Aaron Anderson]

This new factorisation would be pretty useful for talking about multiplicative functions, and maybe other things, I'm interested to see if anyone else is interested in it. Probably the next thing to do with that would be to show that it's order isomorphic and add_monoid isomorphic to factor_multiset, and then a bunch of the sorried properties will probably be reduced to lemmas saying that lattices respect order isomorphisms, which either should exist or do already

[Johan Commelin]

@Aaron Anderson Note that there is already an isomorphism between multiset X and finsupp X nat. You could use that to transport the definition and a bunch of lemmas...
Alternatively, we might decide that the finsupp approach is the more flexible point of view, and just ditch the multiset approach completely.

[Aaron Anderson]

I’ve used .to_multiset to define it, and I know that’s invertible and a strict_mono. Is that the isomorphism you’re referring to?

[Johan Commelin]

Yup, exactly

[Johan Commelin]

The inverse is .to_finsupp

[Aaron Anderson]

I made a new commit, and started a PR review thread for 3094.