Divisibility and Parity in Natural and Integer Arithmetic

We present a collection of formally verified theorems concerning divisibility and parity in natural and integer arithmetic. The results include the transitivity of divisibility over the integers, fundamental parity properties of natural numbers (every natural is either even or odd), the classical theorem that a square being even implies its root is even, and several related closure properties. All proofs are machine-checked using the Lean 4 theorem prover via the Platonic kernel, requiring zero axioms beyond the standard type theory. The formalization demonstrates that elementary number-theoretic reasoning about divisibility and parity can be fully automated through a combination of induction, case analysis, and linear/nonlinear arithmetic tactics. We verify 10 theorems with complete proofs.

Keywords: divisibility, parity, formal verification, Lean 4, natural numbers, integers

MSC 2020: 11A05 (Multiplicative structure; Euclidean algorithm; greatest common divisors), 03B35 (Mechanization of proofs and logical operations)