Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Definition in prerequisite notation
¬n = 0 ∧ (∀ x. Prime(x) → Le(x,n) → ¬Dvd(x · x,n))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
((~(((n)) = 0)) /\ (forall sfd_prime_prioritylayer. (~((sfd_prime_prioritylayer) = 1) /\ forall pvs_left_prioritylayerdomain pvs_right_prioritylayerdomain. (sfd_prime_prioritylayer) = pvs_left_prioritylayerdomain * pvs_right_prioritylayerdomain -> pvs_left_prioritylayerdomain = 1 \/ pvs_right_prioritylayerdomain = 1) -> (exists pvs_le_gap_prioritylayerbound. pvs_le_gap_prioritylayerbound + (sfd_prime_prioritylayer) = ((n))) -> ~(exists pvs_factor_prioritylayersquare. ((n)) = (sfd_prime_prioritylayer * sfd_prime_prioritylayer) * pvs_factor_prioritylayersquare)))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.