Sorting divisors

Stream: new members

[Nathan]

How can I formalize (in Lean) this statement from an IMO problem?

Let $n\geq 2$ be a positive integer, with divisors $1=d_1<d_2<\ldots <d_k =n$. Prove that $d_1 d_2+d_2 d_3 + \ldots + d_{k-1} d_k$ is always less than $n^2$, and determine when it is a divisor of $n^2$.

I initially tried using Finset.sort Nat.lt n.divisors but I get the error "failed to synthesize DecidableRel Nat.lt". I also considered defining $d_i$ recursively, as the minimum of the set of divisors that are bigger than $d_{i-1}$.

[Ruben Van de Velde]

I don't think you should use Nat.lt directly. Does (. < .) work?

[Nathan]

Screenshot 2025-09-26 at 2.10.20 AM.png
no, it doesn't seem to

[Nathan]

oh wait

[Nathan]

(. ≤ .) seems to work

[Nathan]

thanks :pray:

[Nathan]

sort produces a List. I wonder, are lists the right approach here?

[Nathan]

my goal is to prove the solution to the problem

[Ruben Van de Velde]

Yes, I think you want a list, and then probably sum over Finset.range n? You'll want to start your indices from 0 as well

[Nathan]

Shouldn't I sum over something like Finset.range (n.divisors.card-1)?

[Ruben Van de Velde]

Uh, yes, confused my variables there

[Nathan]

Is this right? I'm not sure how to prove h1, h2

import MIL.Common

section p_1_12_13
  def divi (n i : ℕ) (h : i < n.divisors.card) :=
    let d := n.divisors.sort (. ≤ .)
    have h : d.length = n.divisors.card := Multiset.length_sort (. ≤ .)
    d[i]

  def sumdiv (n : ℕ) :=
    ∑ i : Finset.Icc 0 (n.divisors.card-2),
      have h₁ : i < n.divisors.card := sorry
      have h₂ : i+1 < n.divisors.card := sorry
      (divi n i h₁) * (divi n (i+1) h₂)

  example : sumdiv 4 = 10 := sorry

  theorem t1 (n : ℕ) (h : n ≥ 2) : sumdiv n < n^2 := sorry
end p_1_12_13

[Jireh Loreaux]

import Mathlib

example (n : ℕ) :
    letI sorted_divisors := n.divisors.sort (· ≤ ·)
    (List.zipWith (· * ·) (0 :: sorted_divisors) sorted_divisors).sum < n ^ 2 := by
  sorry

[Nathan]

I see! thanks :pray: This avoids indices. I'll try to make some progress with the proof later.

[Nathan]

I think I still might need something like divi (which I defined above), because I want to use $d_i\geq i$. The proof goes like this:

$$\sum_{i=1}^{k-1}d_i d_{i+1}=\sum_{i=1}^{k-1}d_{k-i}d_{k-i+1}=\sum_{i=1}^{k-1}\frac{n}{d_{i+1}}\cdot\frac{n}{d_{i}}\leq n^2\sum_{i=1}^{k-1}\frac{1}{i(i+1)}$$

So won't I need something that maps $i \mapsto d_i$?

[Nathan]

I found a lot of helpful things in Mathlib like List.sum_le_sum and Nat.image_div_divisors_eq_divisors but I wasn't able to put them together into anything coherent.