number

Stream: new members

[BANGJI HU]

Let n be a positive integer. All numbers m which are coprime to n all satisfy m^6 = 1 (mod n) . Find the maximum possible value of n.

[BANGJI HU]

import Mathlib.NumberTheory.Basic -- 导入基础数论库


def coprime (a b : ℕ) : Prop := Nat.gcd a b = 1


def satisfiesMod6 (m n : ℕ) : Bool := (m ^ 6) % n == 1


def allCoprimeSatisfyDec (n : ℕ) : Bool :=
  (List.range n).all (fun m => if Nat.gcd m n == 1 then satisfiesMod6 m n else true)


def findMaxN (current maxN : ℕ) : ℕ :=
  if current = 0 then maxN
  else if allCoprimeSatisfyDec current then findMaxN (current - 1) current
  else findMaxN (current - 1) maxN


def maxValidN : ℕ := findMaxN 9 0

#eval maxValidN

[BANGJI HU]

why does the output is 2 rather then 504

[Trebor Huang]

You started the search at 9 (and you are searching downwards), so it found the largest one below 9, which is 2.

[Notification Bot]

This topic was moved here from #mathlib4 > number by Eric Wieser.

[BANGJI HU]

Trebor Huang said:

You started the search at 9 (and you are searching downwards), so it found the largest one below 9, which is 2.

I only know how to validate in the range but I don't know how to formalize the proposition and especially to find the maximum, the key to my problem is how to prove that 504 is the maximum with lean

[BANGJI HU]

@Trebor Huang