Erdős Problem 445

Exercise 445 · Erdős

Small example: for $p=5$ , $c=1$ , $n=0$ , the pair $(2,3) \in (0,5)$ satisfies $2 \cdot 3 = 6 \equiv 1 \pmod{5}$ .

Formal statement · Lean 4.lean

theorem erdos_445.test.small_example : Erdos445Prop 1 5 1 := by
  sorry

Proof. sorry

Nobody has tried yet.