Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2015P5

import Mathlib
import Mathlib.Tactic

/-!
# USA Mathematical Olympiad 2015, Problem 5

Let a, b, c, d, e be distinct positive integers such that a⁴+b⁴ = c⁴+d⁴ = e⁵.
Show that ac+bd is a composite number.
-/

namespace Usa2015P5

variable { a b c d e p : ℕ }
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (he : 0 < e)
    (habe : a ^ 4 + b ^ 4 = e ^ 5)
    (hcde : c ^ 4 + d ^ 4 = e ^ 5)
    (hab : a ≠ b) (hac : a ≠ c) (had : a ≠ d) (hae : a ≠ e)
    (hbc : b ≠ c) (hbd : b ≠ d) (hbe : b ≠ e)
    (hcd : c ≠ d) (hce : c ≠ e)
    (hde : d ≠ e)

include ha hb hc hd he habe hcde had hbc hac in
theorem usa2015_p5 : ¬ Nat.Prime (a * c + b * d) ∧ (1 < a * c + b * d) := sorry

end Usa2015P5

File author(s): Evan Chen, Kenny Lau, Jujian Zhang

This problem has a complete formalized solution.