gistfile1.txt

import Mathlib

/-- Call `sage` -/
def sageOutput (args : Array String) : IO String := do
  IO.Process.run { cmd := "sage", args := args }

/-- Parse a string containing a list of integers. Should be a proper parser! -/
def String.parseNatList (l : String) : List ℕ :=
  (((l.drop 1).dropRight 2).split (. = ' ')).map
    (fun s => s.stripSuffix ",") |> .map String.toNat!

/-- An "unsafe" function that calls `sage` to find the prime factors of a number. -/
unsafe def sagePrimeFactorsUnsafe (n : ℕ) : List ℕ :=
  let args := #["-c", s!"print(prime_factors({n}))"] ;
  match unsafeBaseIO (sageOutput args).toBaseIO with
  | .ok l => l.parseNatList
  | .error _ => []

/--
An "opaque" wrapper around the unsafe function.

This prevents the `unsafe` label propagating to definitions that use it,
but also prevent Lean from knowing anything about the implementation.
-/
@[implemented_by sagePrimeFactorsUnsafe]
opaque sagePrimeFactors (n : ℕ) : List ℕ

def p := 22801763489

/-- info: [2, 7, 47, 309403] -/
#guard_msgs in
#eval sagePrimeFactors (p - 1)

def rdiv (n : ℕ) (m : ℕ) : ℕ := if n % m = 0 then rdiv (n / m) m else n
decreasing_by sorry

def rdiv' (n : ℕ) (ms : List ℕ) : ℕ := ms.foldl rdiv n

def safePrimeFactors (n : ℕ) : Finset ℕ :=
  let candidates := sagePrimeFactors n
  if candidates.all Nat.Prime && rdiv' n candidates = 1 then
    candidates.toFinset
  else
    Nat.primeFactors n

theorem safePrimeFactors_eq_primeFactors {n : ℕ} : safePrimeFactors n = Nat.primeFactors n := by
  sorry