Divisibility of Consecutive Products
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Abstract
We prove two classical divisibility results for products of consecutive integers: that the product of any two consecutive natural numbers is even, and that the product of any three consecutive natural numbers is divisible by 6. Both results are established by mathematical induction within a formally verified framework. The proofs are entirely elementary, requiring no axioms beyond the Peano axioms for natural numbers. The formalization comprises 2 verified theorems with 0 axioms, demonstrating complete proof coverage for these fundamental number-theoretic facts.
Keywords: consecutive integers, divisibility, induction, elementary number theory
MSC 2020: 11A05 (Multiplicative structure), 11A07 (Congruences)
Length
1,160 words
Claims
4 theorems
Status
draft
Target
pure_math