prime_fourth_power_mod_240

Original target

The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.

Effort & telemetry

Difficulty

4

Runs

1

Successes

1

Provider attempts

1

Statement

The Lean statement the swarm proved, kernel-verified at Gate A.

import Mathlib

theorem prime_fourth_power_mod_240 (p : ℕ) (hp : Nat.Prime p) (h : 5 < p) : p ^ 4 % 240 = 1 := by
  sorry