On defining biggest proper divisors

Stream: new members

[Patrik Cvetek]

Hello, i have just read most of mathematics in lean book and now i would like to formalize something on my own.
This is the problem statement (It is P4 from this year IMO)

A proper divisor of a positive integer $N$ is a positive divisor of $N$ other than $N$ itself.

The infinite sequence $a_1, a_2, \cdots$ consists of positive integers, each of which has at least three proper divisors. For each $n\geq 1$, the integer $a_{n+1}$ is the sum of the three largest proper divisors of $a_n$.

Determine all possible values of $a_1$.

And this is how i formalized the statement (not the solution yet)

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Nat.Factorization.Basic
import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Tactic
import Mathlib.NumberTheory.Divisors

set_option linter.style.commandStart false


def good_number (N : ℕ) : Prop :=
  N.divisors.card ≥ 4

def sdiv1 (n : ℕ) (h : good_number n) :=  (n.divisors.erase (1)).min'  (by sorry)

def sdiv2 (n : ℕ) (h : good_number n) :=  ((n.divisors.erase (1)).erase (sdiv1 n h)).min' (by sorry)

def sdiv3 (n : ℕ) (h : good_number n) :=
  (((n.divisors.erase (1)).erase (sdiv1 n h)).erase (sdiv2 n h)).min' (by sorry)

def bdiv1 (n : ℕ) (h : good_number n) := n / sdiv1 n h
def bdiv2 (n : ℕ) (h : good_number n) := n / sdiv2 n h
def bdiv3 (n : ℕ) (h : good_number n) := n / sdiv3 n h

structure seq (f : ℕ → ℕ) where
  good : ∀ n : ℕ , good_number (f n )
  sum_of_good :
    ∀ n : ℕ , f (n + 1) = bdiv1 (f n) (good n) + bdiv2 (f n) (good n) + bdiv3 (f n) (good n)

def solutionSet := {m | ∃ k₁ k₂, m = 12^(k₁) * 6 * k₂ ∧ k₂.Coprime 10 }

theorem P4 :
  (∀f ,  seq f → f 0 ∈ solutionSet ) ∧ ∀ n ∈ solutionSet , ∃ f , f 0 = n ∧ seq f := by
    sorry

The reason i defined biggest divisors in terms of smallest is because that (should) help in the solution. Now the question is : is this a good way of defining biggest proper divisors or is there something in mathlib or just a better way that will make my job easier. (I am asking this now because i think that feedback might help me formalize this in a "more simple way"). (Btw i have filled all the by sorry myself but removed the proofs for visibility)

[Joseph Myers]

In IMOLean I stated this as

/-- The answer to be determined. -/
def answer : Set ℕ := sorry

theorem result : {a₁ | ∃ a : ℕ → ℕ, a 0 = a₁ ∧ ∀ i, 0 < a i ∧ 3 ≤ #(Nat.properDivisors (a i)) ∧
    a (i + 1) = (((Nat.properDivisors (a i)).sort (· ≤ ·)).reverse.take 3).sum} = answer := by
  sorry

You could debate whether avoiding ≥ should apply in this case of sorting (of course there ought to be a lemma somewhere relating sorting on a relation and then reversing with sorting on the reverse of that relation), but I think the principle of using properDivisors and taking three elements from a sorted list is sound.

Relating the biggest divisors or proper divisors to the smallest isn't something that belongs in the statement of a problem like this; rather, it belongs in API lemmas in mathlib (it's a common thing to do when working with a sorted list of divisors, not at all specific to this problem, so clearly belongs in mathlib proper). Then the proof of such a problem can use those API lemmas to translate the problem statement into whatever form is convenient.

[Patrik Cvetek]

Thanks, but this makes it a little harder. So i will first try and solve it using my definitions (to get the idea of using lean) then i will try to redo it using your problem statement. Should i (and where) make a pull request when (if) done (formalizing your statement)?

[Jakub Nowak]

You can add this to Compfiles:
https://dwrensha.github.io/compfiles/imo.html

[Jakub Nowak]

Patrik Cvetek said:

Thanks, but this makes it a little harder. So i will first try and solve it using my definitions (to get the idea of using lean) then i will try to redo it using your problem statement. Should i (and where) make a pull request when (if) done (formalizing your statement)?

The main problem is probably establishing the fact, that the multiplication of second and last element of properDivisors is equal to n. Once you have that, the definition doesn't really matter that much, you can easily move between one and the other using the theorem that states that fact and rw/simp.