Disproving a conjecture on highly abundant numbers

Stream: general

[François G. Dorais]

The conjecture is that lcm(1,2, ...,n) is always highly abundant (its sum of divisors is larger than that of all previous numbers). This was proven false very recently by Terry Tao on MathOverflow: https://mathoverflow.net/questions/501066/is-the-least-common-multiple-sequence-textlcm1-2-dots-n-a-subset-of-t

There have been even more developments in that thread. Can Lean verify this right now? Is this something that Lean could have verified in "real time"? Could Lean have played an earlier role in this?

I don't have the expertise to verify this quickly myself, but I think it's an interesting test case for interested Lean number theory experts.

CC: @Kevin Buzzard

[Bhavik Mehta]

This is something Lean can verify right now, I have adhoc code to do similar calculations. But from what I have, my setup wouldn't have been able to find this on its own

[François G. Dorais]

Progress is still ongoing on MO so there are opportunities for Lean users to verify the results.

[Notification Bot]

This topic was moved here from #general > Disproving a conjecture on hyperabundant numbers by François G. Dorais.

[François G. Dorais]

This is just correcting the title from "hyper abundant numbers" to "highly abundant numbers". My mistake!

[J. J. Issai (project started by GRP)]

François G. Dorais said:

There have been even more developments in that thread. Can Lean verify this right now? Is this something that Lean could have verified in "real time"? Could Lean have played an earlier role in this?

As an (un-)knowledgeable observer, my guess is that if Terry thought Lean was ready to do this in real time, he would have had Lean do so. As a check on Lean's power, find out how long it takes Lean to generate highly abundant numbers up to L_71. I don't think the system could show a number is not highly abundant without a lot of prompting. As far as verification, I imagine a few experts here could code up the relevant conditions quickly, but I would be surprised if a Lean proof for this appears this month, even if only to show which lcms are not highly abundant for n < 200.

While Lean could have played an earlier role, it is unclear to me how big a role it could take on. I can imagine a determined individual formalizing a proof of L_71 not being highly abundant, using a specific smaller HA number as counterexample, but to take care of ranges of n to show L_n for n in that range is/is not HA is something that will take a while to code. (I can see GH_from_MO's proof of L_n not being HA for n large enough being verified sometime this month.)

I would enjoy the above claims being proved wrong, however. (post by Gerhard Paseman.)

[Ruben Van de Velde]

I think the question was about verifying the example in lean, not finding the specific example.

(Are multiple people using your zulip account? I'm not sure that's allowed here.)

[François G. Dorais]

More specifically, the smallest counterexample was found and it was moreover found that the conjecture is eventually false. There is still a gap in between. Lean should be able to verify the two claims. The real question is how fast Lean could come up with a formal verification. Could it be done in real time?

[Bhavik Mehta]

Here is a formal disproof of the conjecture, using L_71, and the idea from the post by GH from MO.

import Mathlib

open Nat ArithmeticFunction

-- definition of highly abundant number
def IsHighlyAbundant (N : ℕ) : Prop :=
  ∀ m > 0, m < N → σ 1 m < σ 1 N

-- definition of lcm of a range of numbers
def lcmRange (n : ℕ) : ℕ := List.foldl Nat.lcm 1 (List.range' 1 n)

-- a few small examples of lcmRange
example : lcmRange 1 = 1 := rfl
example : lcmRange 2 = 2 := rfl
example : lcmRange 6 = 60 := rfl

-- two lemmas missing from mathlib
lemma sigma_one_apply_prime {p : ℕ} (hp : p.Prime) : σ 1 p = p + 1 := by
  have : σ 1 p = σ 1 (p ^ 1) := by simp
  rw [this, sigma_one_apply_prime_pow hp]
  simp

lemma sigma_one_apply_prime_pow' {p k : ℕ} (hp : p.Prime) :
    σ 1 (p ^ k) = (p ^ (k + 1) - 1) / (p - 1) := by
  rw [sigma_one_apply_prime_pow hp, Nat.geomSum_eq]
  exact hp.two_le

namespace verify_l71

-- the choice of L to verify that the conjecture fails at 71
def L : ℕ := lcmRange 71

-- prove L is what we say it is
example : L = 5624043567677125526551547131200 := by decide +kernel

-- we follow the proof given by "GH from MO"
def L' : ℕ := 7 ^ 2 * 11 * 13 * 17 * 19 * 23 * 29 * 31 * 37 * 41 * 43 * 47 * 53 * 59 * 61

def M : ℕ := 2 ^ 8 * 3 ^ 4 * 5 ^ 3 * 79 * L'

lemma L_eq : L = 205502400 * L' := by decide +kernel
lemma coprime_L'L : Nat.gcd (2 ^ 6 * 3 ^ 3 * 5 ^ 2 * 67 * 71) L' = 1 := by decide +kernel
lemma L_eq' : L = 2 ^ 6 * 3 ^ 3 * 5 ^ 2 * 67 * 71 * L' := by decide +kernel

lemma M_eq : M = 204768000 * L' := rfl
lemma coprime_L'M : Nat.gcd (2 ^ 8 * 3 ^ 4 * 5 ^ 3 * 79) L' = 1 := by decide +kernel
lemma M_eq' : M = 2 ^ 8 * 3 ^ 4 * 5 ^ 3 * 79 * L' := by decide +kernel

lemma M_lt_L : M < L := by decide +kernel

lemma sigma_L_aux : σ 1 (2 ^ 6 * 3 ^ 3 * 5 ^ 2 * 67 * 71) = 771022080 := by
  repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
  repeat rw [sigma_one_apply_prime_pow' (by norm_num)]
  repeat rw [sigma_one_apply_prime (by norm_num)]
  rfl

lemma sigma_M_aux : σ 1 (2 ^ 8 * 3 ^ 4 * 5 ^ 3 * 79) = 771650880 := by
  repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
  repeat rw [sigma_one_apply_prime_pow (by norm_num)]
  repeat rw [sigma_one_apply_prime (by norm_num)]
  rfl

-- the main result: L is not highly abundant
theorem not_HA_L71 : ¬ IsHighlyAbundant L := by
  intro h
  specialize h M (by decide +kernel) M_lt_L
  rw [L_eq', M_eq', isMultiplicative_sigma.map_mul_of_coprime coprime_L'M,
    isMultiplicative_sigma.map_mul_of_coprime coprime_L'L] at h
  simp only [sigma_M_aux, sigma_L_aux] at h
  simpa using Nat.lt_of_mul_lt_mul_right h

-- there exists an n (namely 71) such that lcmRange n is not highly abundant
theorem conjecture_fails : ∃ n, ¬ IsHighlyAbundant (lcmRange n) := ⟨71, not_HA_L71⟩

end verify_l71

[Aaron Liu]

have you seen docs#Finset.lcm

[Bhavik Mehta]

That works too, I guess :)

[Bhavik Mehta]

here's something you might like Aaron, the simp only in the penultimate theorem, can you make it so rw works there?

[Aaron Liu]

like this?

-- the main result: L is not highly abundant
theorem not_HA_L71 : ¬ IsHighlyAbundant L := by
  intro h
  specialize h M (by decide +kernel) M_lt_L
  rw [L_eq', M_eq', isMultiplicative_sigma.map_mul_of_coprime coprime_L'M,
    isMultiplicative_sigma.map_mul_of_coprime coprime_L'L] at h
  conv_lhs at h => rw [sigma_M_aux]
  conv_rhs at h => rw [sigma_L_aux]
  simpa using Nat.lt_of_mul_lt_mul_right h

[Bhavik Mehta]

ah! i was hoping for one rw block, but that confirms my suspicion about why that doesn't work

[Aaron Liu]

or this

-- the main result: L is not highly abundant
theorem not_HA_L71 : ¬ IsHighlyAbundant L := by
  intro h
  specialize h M (by decide +kernel) M_lt_L
  rw [L_eq', M_eq', isMultiplicative_sigma.map_mul_of_coprime coprime_L'M,
    isMultiplicative_sigma.map_mul_of_coprime coprime_L'L] at h
  have hM := sigma_M_aux
  have hL := sigma_L_aux
  generalize σ 1 = s at h hM hL
  rw [hM, hL] at h
  simpa using Nat.lt_of_mul_lt_mul_right h

[Bhavik Mehta]

that's interesting, so it's because it tries to reduce the σ 1 rather than L'? what happens if you generalise that instead

[Aaron Liu]

I thought it would break

-- the main result: L is not highly abundant
theorem not_HA_L71 : ¬ IsHighlyAbundant L := by
  intro h
  specialize h M (by decide +kernel) M_lt_L
  rw [L_eq', M_eq', isMultiplicative_sigma.map_mul_of_coprime coprime_L'M,
    isMultiplicative_sigma.map_mul_of_coprime coprime_L'L] at h
  generalize L' = L' at h
  rw [sigma_M_aux, sigma_L_aux] at h
  simpa using Nat.lt_of_mul_lt_mul_right h

[Bhavik Mehta]

perfect, I hoped it wouldn't! Thanks for these experiments :)

[François G. Dorais]

Bhavik posted an answer on MO: https://mathoverflow.net/a/501238

[Terence Tao]

Thanks for this! Presumably many of the other disproofs for small n can be accomplished by a similar method (especially now that we have set up a table of multipliers in the MO thread). The disproof for sufficiently large n requires the prime number theorem; with the formalization from the PNT+ project it should be possible, with some moderate effort, to show that the conjecture is false for all sufficiently large n with an unspecified bound on "sufficiently large", but until some effective PNT results are formalized (which is something I am actually just starting to work on with some partners) one won't get an explicit bound for this.

Of intermediate difficulty would be the task of formalizing a positive result, and specifically that $L_{67}$ is highly abundant. @Matthew Bolan has a nice computational proof that proceeds by first limiting the prime factorization of any proposed competitor to a limited number of ranges, and then doing a brute force search over something like $10^6$ remaining candidates. The first step seems doable in Lean (perhaps using exact arithmetic and avoiding the use of logarithms), but the latter might be a bit much for the Lean kernel.

[Bhavik Mehta]

I just finished writing down the next two disproofs, in a slightly cleaner style, and in a way that should be easier to make a custom tactic for, then we can just automatically verify the table of counterexamples.
(This code block should be pasted after the earlier one I posted)

lemma not_HA_73 : ¬ IsHighlyAbundant (lcmRange 73) := by
  intro h
  set L : ℕ := lcmRange 73
  set l : ℕ := 2 ^ 6 * 3 ^ 3 * 5 ^ 2 * 67 * 71
  set K : ℕ := L / l
  set m : ℕ := 2 ^ 8 * 3 ^ 4 * 5 ^ 3 * 79
  set M : ℕ := m * K with hM
  have hL : L = l * K := by decide +kernel
  have hLK : Nat.gcd l K = 1 := by decide +kernel
  have hMK : Nat.gcd m K = 1 := by decide +kernel
  have hK : 0 < K := by decide +kernel
  clear_value K
  have hσL : σ₁ l = 771022080 := by
    repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
    repeat rw [sigma_one_apply_prime_pow' (by norm_num)]
    repeat rw [sigma_one_apply_prime (by norm_num)]
    rfl
  have hσM : σ₁ m = 771650880 := by
    repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
    repeat rw [sigma_one_apply_prime_pow (by norm_num)]
    repeat rw [sigma_one_apply_prime (by norm_num)]
    rfl
  have := h M (by cutsat) (by cutsat)
  rw [hM, hL, isMultiplicative_sigma.map_mul_of_coprime hMK,
    isMultiplicative_sigma.map_mul_of_coprime hLK, hσL, hσM] at this
  cutsat

lemma not_HA_79 : ¬ IsHighlyAbundant (lcmRange 79) := by
  intro h
  set L : ℕ := lcmRange 79
  set l : ℕ := 2 ^ 6 * 3 ^ 3 * 5 ^ 2 * 11 * 67 * 79
  set K : ℕ := L / l
  set m : ℕ := 2 ^ (6 + 5) * 3 ^ (3 + 1) * 5 ^ (2 + 1) * 11 ^ 2
  set M : ℕ := m * K with hM
  have hL : L = l * K := by decide +kernel
  have hLK : Nat.gcd l K = 1 := by decide +kernel
  have hMK : Nat.gcd m K = 1 := by decide +kernel
  have hK : 0 < K := by decide +kernel
  clear_value K
  have hσL : σ₁ l = 10280294400 := by
    repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
    repeat rw [sigma_one_apply_prime_pow' (by norm_num)]
    repeat rw [sigma_one_apply_prime (by norm_num)]
    rfl
  have hσM : σ₁ m = 10280530260 := by
    repeat rw [isMultiplicative_sigma.map_mul_of_coprime rfl]
    repeat rw [sigma_one_apply_prime_pow' (by norm_num)]
    rfl
  have := h M (by cutsat) (by cutsat)
  rw [hM, hL, isMultiplicative_sigma.map_mul_of_coprime hMK,
    isMultiplicative_sigma.map_mul_of_coprime hLK, hσL, hσM] at this
  cutsat

[Bhavik Mehta]

Here is partial progress towards a formalisation of (the second part) of Bolan's approach, and a setup for the disproof for large n. https://gist.github.com/b-mehta/75d7f118e5bb6440c131c4c6ceaf7478

I also have a lean proof (not posted) that the sum of (p - 1) / p ^ 2 over the first 1000 primes is more than 401/200, which is used in GH from MO's proof. To be explicit about this one: I wrote down the first 1000 primes in lean, and the kernel has accepted that they are all primes, and that the sum of that function over them is more than 401/200: I haven't checked that they are indeed the first 1000 primes, but this shouldn't be needed for that argument to go through.

[Bhavik Mehta]

And finally, I've added disproofs for all the small n listed in the table on MO: https://gist.github.com/b-mehta/75d7f118e5bb6440c131c4c6ceaf7478#file-highly_abundant_small-lean.

[Terence Tao]

Max Alekseyev has an alternate way to verify the highly abundant property that works well in SAGE due to its support for parallel computation, but may be trickier to implement in Lean. I also have an alternate theoretical approach to the asymptotic regime that requires "only" the prime number theorem, rather than the prime number theorem in arithmetic progressions. (Both are listed as answers on the MO site.)

[Terence Tao]

Matthew Bolan has constructed a "ladder" of 3477 different prime additions and subtractions that, between them, cover all counterexamples up to $n=10^{10}$. I am slightly curious as to your opinion as to whether such a ladder could be comfortably elaborated by the Lean kernel, or whether some shortening of this ladder would be desirable first before trying to do a Lean conversion (which would presumably be a rather mechanical extension of the proofs already provided).

[Bhavik Mehta]

My guess is that it'd be easier to use his "medium" ladder up to 200000, and use the choices of six primes he found together with your six prime condition for the numbers between 200000 and 10^10. My reasoning here is that the limiting factor is how much time Lean would spend on each "rung", which in the case of the addition/subtraction method requires three calculations per n (in my current approach, at least), whereas for the six prime method it should suffice to check inequalities at endpoints, meaning it shouldn't depend on the number of n per rung.

Ah, although I think I can improve my verification procedure for the addition/subtraction mode, let me experiment some more...

[Bhavik Mehta]

The experiment worked, I've verified all the counterexamples up to $n = 10^5$ now. At this range, each rung is checked by Lean in a matter of seconds (on my slow laptop). It looks like the current time-to-compile is linear in $n$.
To be specific, that's a sorry-free proof of

theorem smallish : ∀ i ∈ Finset.Icc 173 100000, ¬ IsHighlyAbundant (lcmRange i)

I have a pretty clear idea in my mind of how I can push this to be much faster, and I hope the proof up to $n = 10^{10}$ can be made to, when it's written, compile within a few hours at most. So, I'll hold off posting code for now, because I think the next version will be a lot faster and cleaner.

[Bhavik Mehta]

I've now managed to verify all the counterexamples up to 2 billion, with the help of @Matthew Bolan and his improved ladder. But the ladder goes up to $10^{10}$, ie 10 billion, and the issue here is verifying large primes. Fortunately, this is an issue which I wrote Lean code to solve earlier in the year, so getting up to 10 billion should be relatively easy now, and then the approach should scale comfortably to $10^{40}$ ish too.

[Bhavik Mehta]

Indeed getting to $10^{10}$ was relatively easy! And my estimate of a few hours for the proof was even more pessimistic than I thought, it compiles in under a minute. The code is here: https://github.com/b-mehta/HighlyAbundant. Let me in particular point out Matthew's ladder https://gist.github.com/mjtb49/b4dd732f2c6fea5c091071c92c955942#file-ladder102-txt and the statement and proof derived from it https://github.com/b-mehta/HighlyAbundant/blob/8350bee92e61118280ad8f7aa683b75406684c9c/HighlyAbundant/ClimbLadder.lean#L28.

[Julia Scheaffer]

What is the reason to use notation "σ₁" => ArithmeticFunction.sigma 1 instead of abbrev σ₁ := ArithmeticFunction.sigma 1?

[Kenny Lau]

abbrev is bad

[Bhavik Mehta]

My reasoning here was nothing deep, I just wanted the statements about it to look nice. In the ArithmeticFunction scope, we have notation for ArithmeticFunction.sigma, so I just copied that but specialised. I doubt things would be much different if I used abbrev

[Bhavik Mehta]

And now we're up to $10^{40}$. The total build time for the proof in CI is just under 12 minutes, and about 10 minutes of that is proving primality of specific large numbers. Current code is in this branch https://github.com/b-mehta/HighlyAbundant/tree/enlarge, which I'll try to optimise before merging to the repo's master.