Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2020P3

import Mathlib

/-!
# USA Mathematical Olympiad 2020 Problem 3

Let p be an odd prime. An integer x is called a *quadratic non-residue* if p does not
divide x − t² for any integer t.

Denote by A the set of all integers a such that 1 ≤ a < p, and both a and 4 − a are
quadratic non-residues. Calculate the remainder when the product of the elements
of A is divided by p.
-/

namespace Usamo2020P3

open Finset ZMod

/- determine -/ abbrev solution_val : ℕ := sorry

theorem usamo2020_p3 (p : ℕ) [hp : Fact (Nat.Prime p)] (hp2 : p ≠ 2) :
    ∏ a ∈ Finset.univ.filter (fun (a : ZMod p) => a ≠ 0 ∧ ¬IsSquare a ∧ ¬IsSquare (4 - a)), a = (solution_val : ZMod p) := sorry

end Usamo2020P3

File author(s): Daniel Liao

This problem has a complete formalized solution.